prefer records with speaking labels over deeply nested tuples
authorhaftmann
Tue Jun 05 07:05:56 2012 +0200 (2012-06-05)
changeset 48072ace701efe203
parent 48071 d7864276bca8
child 48073 1b609a7837ef
prefer records with speaking labels over deeply nested tuples
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Tools/list_code.ML
src/HOL/Tools/numeral.ML
src/HOL/Tools/string_code.ML
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_simp.ML
src/Tools/Code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jun 04 12:55:54 2012 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jun 05 07:05:56 2012 +0200
     1.3 @@ -633,8 +633,12 @@
     1.4      (*assumption: dummy values are not relevant for serialization*)
     1.5      val (unitt, unitT) = case lookup_const naming @{const_name Unity}
     1.6       of SOME unit' =>
     1.7 -        let val unitT = the (lookup_tyco naming @{type_name unit}) `%% []
     1.8 -        in (IConst (unit', ((([], []), ([], unitT)), false)), unitT) end
     1.9 +          let
    1.10 +            val unitT = the (lookup_tyco naming @{type_name unit}) `%% []
    1.11 +          in
    1.12 +            (IConst { name = unit', typargs = [], dicts = [], dom = [],
    1.13 +              range = unitT, annotate = false }, unitT)
    1.14 +          end
    1.15        | NONE => error ("Must include " ^ @{const_name Unity} ^ " in generated constants.");
    1.16      fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
    1.17        | dest_abs (t, ty) =
    1.18 @@ -643,21 +647,21 @@
    1.19              val v = singleton (Name.variant_list vs) "x";
    1.20              val ty' = (hd o fst o unfold_fun) ty;
    1.21            in ((SOME v, ty'), t `$ IVar (SOME v)) end;
    1.22 -    fun force (t as IConst (c, _) `$ t') = if is_return c
    1.23 +    fun force (t as IConst { name = c, ... } `$ t') = if is_return c
    1.24            then t' else t `$ unitt
    1.25        | force t = t `$ unitt;
    1.26      fun tr_bind'' [(t1, _), (t2, ty2)] =
    1.27        let
    1.28          val ((v, ty), t) = dest_abs (t2, ty2);
    1.29 -      in ICase (((force t1, ty), [(IVar v, tr_bind' t)]), dummy_case_term) end
    1.30 +      in ICase { term = force t1, typ = ty, clauses = [(IVar v, tr_bind' t)], primitive = dummy_case_term } end
    1.31      and tr_bind' t = case unfold_app t
    1.32 -     of (IConst (c, ((_, (ty1 :: ty2 :: _, _)), _)), [x1, x2]) => if is_bind c
    1.33 +     of (IConst { name = c, dom = ty1 :: ty2 :: _, ... }, [x1, x2]) => if is_bind c
    1.34            then tr_bind'' [(x1, ty1), (x2, ty2)]
    1.35            else force t
    1.36        | _ => force t;
    1.37 -    fun imp_monad_bind'' ts = (SOME dummy_name, unitT) `|=> ICase (((IVar (SOME dummy_name), unitT),
    1.38 -      [(unitt, tr_bind'' ts)]), dummy_case_term)
    1.39 -    fun imp_monad_bind' (const as (c, ((_, (tys, _)), _))) ts = if is_bind c then case (ts, tys)
    1.40 +    fun imp_monad_bind'' ts = (SOME dummy_name, unitT) `|=>
    1.41 +      ICase { term = IVar (SOME dummy_name), typ = unitT, clauses = [(unitt, tr_bind'' ts)], primitive = dummy_case_term }
    1.42 +    fun imp_monad_bind' (const as { name = c, dom = dom, ... }) ts = if is_bind c then case (ts, dom)
    1.43         of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)]
    1.44          | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3
    1.45          | (ts, _) => imp_monad_bind (eta_expand 2 (const, ts))
    1.46 @@ -668,10 +672,9 @@
    1.47           of (IConst const, ts) => imp_monad_bind' const ts
    1.48            | (t, ts) => imp_monad_bind t `$$ map imp_monad_bind ts)
    1.49        | imp_monad_bind (v_ty `|=> t) = v_ty `|=> imp_monad_bind t
    1.50 -      | imp_monad_bind (ICase (((t, ty), pats), t0)) = ICase
    1.51 -          (((imp_monad_bind t, ty),
    1.52 -            (map o pairself) imp_monad_bind pats),
    1.53 -              imp_monad_bind t0);
    1.54 +      | imp_monad_bind (ICase { term = t, typ = ty, clauses = clauses, primitive = t0 }) =
    1.55 +          ICase { term = imp_monad_bind t, typ = ty,
    1.56 +            clauses = (map o pairself) imp_monad_bind clauses, primitive = imp_monad_bind t0 };
    1.57  
    1.58    in (Graph.map o K o map_terms_stmt) imp_monad_bind end;
    1.59  
    1.60 @@ -688,3 +691,4 @@
    1.61  hide_const (open) Heap heap guard raise' fold_map
    1.62  
    1.63  end
    1.64 +
     2.1 --- a/src/HOL/Tools/list_code.ML	Mon Jun 04 12:55:54 2012 +0200
     2.2 +++ b/src/HOL/Tools/list_code.ML	Tue Jun 05 07:05:56 2012 +0200
     2.3 @@ -20,14 +20,14 @@
     2.4  
     2.5  fun implode_list nil' cons' t =
     2.6    let
     2.7 -    fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
     2.8 +    fun dest_cons (IConst { name = c, ... } `$ t1 `$ t2) =
     2.9            if c = cons'
    2.10            then SOME (t1, t2)
    2.11            else NONE
    2.12        | dest_cons _ = NONE;
    2.13      val (ts, t') = Code_Thingol.unfoldr dest_cons t;
    2.14    in case t'
    2.15 -   of IConst (c, _) => if c = nil' then SOME ts else NONE
    2.16 +   of IConst { name = c, ... } => if c = nil' then SOME ts else NONE
    2.17      | _ => NONE
    2.18    end;
    2.19  
     3.1 --- a/src/HOL/Tools/numeral.ML	Mon Jun 04 12:55:54 2012 +0200
     3.2 +++ b/src/HOL/Tools/numeral.ML	Tue Jun 05 07:05:56 2012 +0200
     3.3 @@ -69,11 +69,11 @@
     3.4    let
     3.5      fun dest_numeral one' bit0' bit1' thm t =
     3.6        let
     3.7 -        fun dest_bit (IConst (c, _)) = if c = bit0' then 0
     3.8 +        fun dest_bit (IConst { name = c, ... }) = if c = bit0' then 0
     3.9                else if c = bit1' then 1
    3.10                else Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit"
    3.11            | dest_bit _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit";
    3.12 -        fun dest_num (IConst (c, _)) = if c = one' then 1
    3.13 +        fun dest_num (IConst { name = c, ... }) = if c = one' then 1
    3.14                else Code_Printer.eqn_error thm "Illegal numeral expression: illegal leading digit"
    3.15            | dest_num (t1 `$ t2) = 2 * dest_num t2 + dest_bit t1
    3.16            | dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term";
     4.1 --- a/src/HOL/Tools/string_code.ML	Mon Jun 04 12:55:54 2012 +0200
     4.2 +++ b/src/HOL/Tools/string_code.ML	Tue Jun 05 07:05:56 2012 +0200
     4.3 @@ -23,13 +23,13 @@
     4.4        | decode _ ~1 = NONE
     4.5        | decode n m = SOME (chr (n * 16 + m));
     4.6    in case tt
     4.7 -   of (IConst (c1, _), IConst (c2, _)) => decode (idx c1) (idx c2)
     4.8 +   of (IConst { name = c1, ... }, IConst { name = c2, ... }) => decode (idx c1) (idx c2)
     4.9      | _ => NONE
    4.10    end;
    4.11     
    4.12  fun implode_string char' nibbles' mk_char mk_string ts =
    4.13    let
    4.14 -    fun implode_char (IConst (c, _) `$ t1 `$ t2) =
    4.15 +    fun implode_char (IConst { name = c, ... } `$ t1 `$ t2) =
    4.16            if c = char' then decode_char nibbles' (t1, t2) else NONE
    4.17        | implode_char _ = NONE;
    4.18      val ts' = map_filter implode_char ts;
     5.1 --- a/src/Tools/Code/code_haskell.ML	Mon Jun 04 12:55:54 2012 +0200
     5.2 +++ b/src/Tools/Code/code_haskell.ML	Tue Jun 05 07:05:56 2012 +0200
     5.3 @@ -60,8 +60,8 @@
     5.4        print_tyco_expr tyvars NOBR (tyco, map ITyVar vs);
     5.5      fun print_typscheme tyvars (vs, ty) =
     5.6        Pretty.block (print_typforall tyvars vs @ print_typcontext tyvars vs @| print_typ tyvars NOBR ty);
     5.7 -    fun print_term tyvars some_thm vars fxy (IConst c) =
     5.8 -          print_app tyvars some_thm vars fxy (c, [])
     5.9 +    fun print_term tyvars some_thm vars fxy (IConst const) =
    5.10 +          print_app tyvars some_thm vars fxy (const, [])
    5.11        | print_term tyvars some_thm vars fxy (t as (t1 `$ t2)) =
    5.12            (case Code_Thingol.unfold_const_app t
    5.13             of SOME app => print_app tyvars some_thm vars fxy app
    5.14 @@ -79,15 +79,15 @@
    5.15              val (binds, t') = Code_Thingol.unfold_pat_abs t;
    5.16              val (ps, vars') = fold_map (print_bind tyvars some_thm BR o fst) binds vars;
    5.17            in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end
    5.18 -      | print_term tyvars some_thm vars fxy (ICase (cases as (_, t0))) =
    5.19 -          (case Code_Thingol.unfold_const_app t0
    5.20 -           of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
    5.21 -                then print_case tyvars some_thm vars fxy cases
    5.22 -                else print_app tyvars some_thm vars fxy c_ts
    5.23 -            | NONE => print_case tyvars some_thm vars fxy cases)
    5.24 -    and print_app_expr tyvars some_thm vars ((c, ((_, (arg_tys, result_ty)), annotate)), ts) =
    5.25 +      | print_term tyvars some_thm vars fxy (ICase case_expr) =
    5.26 +          (case Code_Thingol.unfold_const_app (#primitive case_expr)
    5.27 +           of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
    5.28 +                then print_case tyvars some_thm vars fxy case_expr
    5.29 +                else print_app tyvars some_thm vars fxy app
    5.30 +            | NONE => print_case tyvars some_thm vars fxy case_expr)
    5.31 +    and print_app_expr tyvars some_thm vars ({ name = c, dom, range, annotate, ... }, ts) =
    5.32        let
    5.33 -        val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (arg_tys, result_ty)
    5.34 +        val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (dom, range)
    5.35          val printed_const =
    5.36            if annotate then
    5.37              brackets [(str o deresolve) c, str "::", print_typ tyvars NOBR ty]
    5.38 @@ -98,9 +98,11 @@
    5.39        end
    5.40      and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax
    5.41      and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
    5.42 -    and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
    5.43 +    and print_case tyvars some_thm vars fxy { clauses = [], ... } =
    5.44 +          (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""]
    5.45 +      | print_case tyvars some_thm vars fxy (case_expr as { clauses = [_], ... }) =
    5.46            let
    5.47 -            val (binds, body) = Code_Thingol.unfold_let (ICase cases);
    5.48 +            val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
    5.49              fun print_match ((pat, _), t) vars =
    5.50                vars
    5.51                |> print_bind tyvars some_thm BR pat
    5.52 @@ -110,7 +112,7 @@
    5.53              ps
    5.54              (concat [str "}", str "in", print_term tyvars some_thm vars' NOBR body])
    5.55            end
    5.56 -      | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
    5.57 +      | print_case tyvars some_thm vars fxy { term = t, typ = ty, clauses = clauses as _ :: _, ... } =
    5.58            let
    5.59              fun print_select (pat, body) =
    5.60                let
    5.61 @@ -119,9 +121,7 @@
    5.62            in Pretty.block_enclose
    5.63              (concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})")
    5.64              (map print_select clauses)
    5.65 -          end
    5.66 -      | print_case tyvars some_thm vars fxy ((_, []), _) =
    5.67 -          (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
    5.68 +          end;
    5.69      fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
    5.70            let
    5.71              val tyvars = intro_vars (map fst vs) reserved;
    5.72 @@ -221,7 +221,7 @@
    5.73                str "};"
    5.74              ) (map print_classparam classparams)
    5.75            end
    5.76 -      | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) =
    5.77 +      | print_stmt (_, Code_Thingol.Classinst { class, tyco, vs, inst_params, ... }) =
    5.78            let
    5.79              val tyvars = intro_vars (map fst vs) reserved;
    5.80              fun requires_args classparam = case const_syntax classparam
    5.81 @@ -237,14 +237,15 @@
    5.82                      ]
    5.83                  | SOME k =>
    5.84                      let
    5.85 -                      val (c, ((_, tys), _)) = const;
    5.86 +                      val { name = c, dom, range, ... } = const;
    5.87                        val (vs, rhs) = (apfst o map) fst
    5.88                          (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
    5.89                        val s = if (is_some o const_syntax) c
    5.90                          then NONE else (SOME o Long_Name.base_name o deresolve) c;
    5.91                        val vars = reserved
    5.92                          |> intro_vars (map_filter I (s :: vs));
    5.93 -                      val lhs = IConst (classparam, ((([], []), tys), false)) `$$ map IVar vs;
    5.94 +                      val lhs = IConst { name = classparam, typargs = [],
    5.95 +                        dicts = [], dom = dom, range = range, annotate = false } `$$ map IVar vs;
    5.96                          (*dictionaries are not relevant at this late stage,
    5.97                            and these consts never need type annotations for disambiguation *)
    5.98                      in
    5.99 @@ -264,7 +265,7 @@
   5.100                  str " where {"
   5.101                ],
   5.102                str "};"
   5.103 -            ) (map print_classparam_instance classparam_instances)
   5.104 +            ) (map print_classparam_instance inst_params)
   5.105            end;
   5.106    in print_stmt end;
   5.107  
   5.108 @@ -407,7 +408,7 @@
   5.109       of SOME ((pat, ty), t') =>
   5.110            SOME ((SOME ((pat, ty), true), t1), t')
   5.111        | NONE => NONE;
   5.112 -    fun dest_monad c_bind_name (IConst (c, _) `$ t1 `$ t2) =
   5.113 +    fun dest_monad c_bind_name (IConst { name = c, ... } `$ t1 `$ t2) =
   5.114            if c = c_bind_name then dest_bind t1 t2
   5.115            else NONE
   5.116        | dest_monad _ t = case Code_Thingol.split_let t
     6.1 --- a/src/Tools/Code/code_ml.ML	Mon Jun 04 12:55:54 2012 +0200
     6.2 +++ b/src/Tools/Code/code_ml.ML	Tue Jun 05 07:05:56 2012 +0200
     6.3 @@ -28,9 +28,10 @@
     6.4  
     6.5  datatype ml_binding =
     6.6      ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
     6.7 -  | ML_Instance of string * ((class * (string * (vname * sort) list))
     6.8 -        * ((class * (string * (string * dict list list))) list
     6.9 -      * (((string * const) * (thm * bool)) list * ((string * const) * (thm * bool)) list)));
    6.10 +  | ML_Instance of string * { class: string, tyco: string, vs: (vname * sort) list,
    6.11 +        superinsts: (class * (string * (string * dict list list))) list,
    6.12 +        inst_params: ((string * const) * (thm * bool)) list,
    6.13 +        superinst_params: ((string * const) * (thm * bool)) list };
    6.14  
    6.15  datatype ml_stmt =
    6.16      ML_Exc of string * (typscheme * int)
    6.17 @@ -83,15 +84,15 @@
    6.18      and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
    6.19      val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
    6.20        (map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort));
    6.21 -    fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
    6.22 -          print_app is_pseudo_fun some_thm vars fxy (c, [])
    6.23 +    fun print_term is_pseudo_fun some_thm vars fxy (IConst const) =
    6.24 +          print_app is_pseudo_fun some_thm vars fxy (const, [])
    6.25        | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
    6.26            str "_"
    6.27        | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =
    6.28            str (lookup_var vars v)
    6.29        | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =
    6.30            (case Code_Thingol.unfold_const_app t
    6.31 -           of SOME c_ts => print_app is_pseudo_fun some_thm vars fxy c_ts
    6.32 +           of SOME app => print_app is_pseudo_fun some_thm vars fxy app
    6.33              | NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1,
    6.34                  print_term is_pseudo_fun some_thm vars BR t2])
    6.35        | print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) =
    6.36 @@ -102,15 +103,15 @@
    6.37                #>> (fn p => concat [str "fn", p, str "=>"]);
    6.38              val (ps, vars') = fold_map print_abs binds vars;
    6.39            in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end
    6.40 -      | print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =
    6.41 -          (case Code_Thingol.unfold_const_app t0
    6.42 -           of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
    6.43 -                then print_case is_pseudo_fun some_thm vars fxy cases
    6.44 -                else print_app is_pseudo_fun some_thm vars fxy c_ts
    6.45 -            | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
    6.46 -    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), (arg_tys, _)), _)), ts)) =
    6.47 +      | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
    6.48 +          (case Code_Thingol.unfold_const_app (#primitive case_expr)
    6.49 +           of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
    6.50 +                then print_case is_pseudo_fun some_thm vars fxy case_expr
    6.51 +                else print_app is_pseudo_fun some_thm vars fxy app
    6.52 +            | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
    6.53 +    and print_app_expr is_pseudo_fun some_thm vars (app as ({ name = c, dicts = dss, dom = dom, ... }, ts)) =
    6.54        if is_cons c then
    6.55 -        let val k = length arg_tys in
    6.56 +        let val k = length dom in
    6.57            if k < 2 orelse length ts = k
    6.58            then (str o deresolve) c
    6.59              :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
    6.60 @@ -118,14 +119,16 @@
    6.61          end
    6.62        else if is_pseudo_fun c
    6.63          then (str o deresolve) c @@ str "()"
    6.64 -      else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
    6.65 +      else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) dss
    6.66          @ map (print_term is_pseudo_fun some_thm vars BR) ts
    6.67      and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
    6.68        (print_term is_pseudo_fun) const_syntax some_thm vars
    6.69      and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
    6.70 -    and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
    6.71 +    and print_case is_pseudo_fun some_thm vars fxy { clauses = [], ... } =
    6.72 +          (concat o map str) ["raise", "Fail", "\"empty case\""]
    6.73 +      | print_case is_pseudo_fun some_thm vars fxy (case_expr as { clauses = [_], ... }) =
    6.74            let
    6.75 -            val (binds, body) = Code_Thingol.unfold_let (ICase cases);
    6.76 +            val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
    6.77              fun print_match ((pat, _), t) vars =
    6.78                vars
    6.79                |> print_bind is_pseudo_fun some_thm NOBR pat
    6.80 @@ -139,7 +142,7 @@
    6.81                str "end"
    6.82              ]
    6.83            end
    6.84 -      | print_case is_pseudo_fun some_thm vars fxy (((t, ty), clause :: clauses), _) =
    6.85 +      | print_case is_pseudo_fun some_thm vars fxy { term = t, typ = ty, clauses = clause :: clauses, ... } =
    6.86            let
    6.87              fun print_select delim (pat, body) =
    6.88                let
    6.89 @@ -154,9 +157,7 @@
    6.90                :: print_select "of" clause
    6.91                :: map (print_select "|") clauses
    6.92              )
    6.93 -          end
    6.94 -      | print_case is_pseudo_fun some_thm vars fxy ((_, []), _) =
    6.95 -          (concat o map str) ["raise", "Fail", "\"empty case\""];
    6.96 +          end;
    6.97      fun print_val_decl print_typscheme (name, typscheme) = concat
    6.98        [str "val", str (deresolve name), str ":", print_typscheme typscheme];
    6.99      fun print_datatype_decl definer (tyco, (vs, cos)) =
   6.100 @@ -206,7 +207,7 @@
   6.101              ))
   6.102            end
   6.103        | print_def is_pseudo_fun _ definer
   6.104 -          (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
   6.105 +          (ML_Instance (inst, { class, tyco, vs, superinsts, inst_params, ... })) =
   6.106            let
   6.107              fun print_super_instance (_, (classrel, x)) =
   6.108                concat [
   6.109 @@ -230,8 +231,8 @@
   6.110                    else print_dict_args vs)
   6.111                @ str "="
   6.112                :: enum "," "{" "}"
   6.113 -                (map print_super_instance super_instances
   6.114 -                  @ map print_classparam_instance classparam_instances)
   6.115 +                (map print_super_instance superinsts
   6.116 +                  @ map print_classparam_instance inst_params)
   6.117                :: str ":"
   6.118                @@ print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs])
   6.119              ))
   6.120 @@ -386,15 +387,15 @@
   6.121      and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
   6.122      val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
   6.123        (map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort));
   6.124 -    fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
   6.125 -          print_app is_pseudo_fun some_thm vars fxy (c, [])
   6.126 +    fun print_term is_pseudo_fun some_thm vars fxy (IConst const) =
   6.127 +          print_app is_pseudo_fun some_thm vars fxy (const, [])
   6.128        | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
   6.129            str "_"
   6.130        | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =
   6.131            str (lookup_var vars v)
   6.132        | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =
   6.133            (case Code_Thingol.unfold_const_app t
   6.134 -           of SOME c_ts => print_app is_pseudo_fun some_thm vars fxy c_ts
   6.135 +           of SOME app => print_app is_pseudo_fun some_thm vars fxy app
   6.136              | NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1,
   6.137                  print_term is_pseudo_fun some_thm vars BR t2])
   6.138        | print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) =
   6.139 @@ -402,15 +403,15 @@
   6.140              val (binds, t') = Code_Thingol.unfold_pat_abs t;
   6.141              val (ps, vars') = fold_map (print_bind is_pseudo_fun some_thm BR o fst) binds vars;
   6.142            in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end
   6.143 -      | print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =
   6.144 -          (case Code_Thingol.unfold_const_app t0
   6.145 -           of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
   6.146 -                then print_case is_pseudo_fun some_thm vars fxy cases
   6.147 -                else print_app is_pseudo_fun some_thm vars fxy c_ts
   6.148 -            | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
   6.149 -    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), (tys, _)), _)), ts)) =
   6.150 +      | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
   6.151 +          (case Code_Thingol.unfold_const_app (#primitive case_expr)
   6.152 +           of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
   6.153 +                then print_case is_pseudo_fun some_thm vars fxy case_expr
   6.154 +                else print_app is_pseudo_fun some_thm vars fxy app
   6.155 +            | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
   6.156 +    and print_app_expr is_pseudo_fun some_thm vars (app as ({ name = c, dicts = dss, dom = dom, ... }, ts)) =
   6.157        if is_cons c then
   6.158 -        let val k = length tys in
   6.159 +        let val k = length dom in
   6.160            if length ts = k
   6.161            then (str o deresolve) c
   6.162              :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
   6.163 @@ -418,14 +419,16 @@
   6.164          end
   6.165        else if is_pseudo_fun c
   6.166          then (str o deresolve) c @@ str "()"
   6.167 -      else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
   6.168 +      else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) dss
   6.169          @ map (print_term is_pseudo_fun some_thm vars BR) ts
   6.170      and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
   6.171        (print_term is_pseudo_fun) const_syntax some_thm vars
   6.172      and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
   6.173 -    and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
   6.174 +    and print_case is_pseudo_fun some_thm vars fxy { clauses = [], ... } =
   6.175 +          (concat o map str) ["failwith", "\"empty case\""]
   6.176 +      | print_case is_pseudo_fun some_thm vars fxy (case_expr as { clauses = [_], ... }) =
   6.177            let
   6.178 -            val (binds, body) = Code_Thingol.unfold_let (ICase cases);
   6.179 +            val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
   6.180              fun print_let ((pat, _), t) vars =
   6.181                vars
   6.182                |> print_bind is_pseudo_fun some_thm NOBR pat
   6.183 @@ -436,7 +439,7 @@
   6.184              brackify_block fxy (Pretty.chunks ps) []
   6.185                (print_term is_pseudo_fun some_thm vars' NOBR body)
   6.186            end
   6.187 -      | print_case is_pseudo_fun some_thm vars fxy (((t, ty), clause :: clauses), _) =
   6.188 +      | print_case is_pseudo_fun some_thm vars fxy { term = t, typ = ty, clauses = clause :: clauses, ... } =
   6.189            let
   6.190              fun print_select delim (pat, body) =
   6.191                let
   6.192 @@ -449,9 +452,7 @@
   6.193                :: print_select "with" clause
   6.194                :: map (print_select "|") clauses
   6.195              )
   6.196 -          end
   6.197 -      | print_case is_pseudo_fun some_thm vars fxy ((_, []), _) =
   6.198 -          (concat o map str) ["failwith", "\"empty case\""];
   6.199 +          end;
   6.200      fun print_val_decl print_typscheme (name, typscheme) = concat
   6.201        [str "val", str (deresolve name), str ":", print_typscheme typscheme];
   6.202      fun print_datatype_decl definer (tyco, (vs, cos)) =
   6.203 @@ -546,7 +547,7 @@
   6.204              ))
   6.205            end
   6.206        | print_def is_pseudo_fun _ definer
   6.207 -            (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
   6.208 +          (ML_Instance (inst, { class, tyco, vs, superinsts, inst_params, ... })) =
   6.209            let
   6.210              fun print_super_instance (_, (classrel, x)) =
   6.211                concat [
   6.212 @@ -570,8 +571,8 @@
   6.213                    else print_dict_args vs)
   6.214                @ str "="
   6.215                @@ brackets [
   6.216 -                enum_default "()" ";" "{" "}" (map print_super_instance super_instances
   6.217 -                  @ map print_classparam_instance classparam_instances),
   6.218 +                enum_default "()" ";" "{" "}" (map print_super_instance superinsts
   6.219 +                  @ map print_classparam_instance inst_params),
   6.220                  str ":",
   6.221                  print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs])
   6.222                ]
   6.223 @@ -731,7 +732,7 @@
   6.224                  | _ => (eqs, NONE)
   6.225                else (eqs, NONE)
   6.226            in (ML_Function (name, (tysm, eqs')), some_value_name) end
   6.227 -      | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, vs)), _))) =
   6.228 +      | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as { vs, ... })) =
   6.229            (ML_Instance (name, stmt), if forall (null o snd) vs then SOME (name, false) else NONE)
   6.230        | ml_binding_of_stmt (name, _) =
   6.231            error ("Binding block containing illegal statement: " ^ labelled_name name)
     7.1 --- a/src/Tools/Code/code_printer.ML	Mon Jun 04 12:55:54 2012 +0200
     7.2 +++ b/src/Tools/Code/code_printer.ML	Tue Jun 05 07:05:56 2012 +0200
     7.3 @@ -315,7 +315,7 @@
     7.4        |-> (fn cs' => pair (Complex_const_syntax (n, f literals cs')));
     7.5  
     7.6  fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
     7.7 -    (app as ((c, ((_, (arg_tys, _)), _)), ts)) =
     7.8 +    (app as ({ name = c, dom, ... }, ts)) =
     7.9    case const_syntax c of
    7.10      NONE => brackify fxy (print_app_expr some_thm vars app)
    7.11    | SOME (Plain_const_syntax (_, s)) =>
    7.12 @@ -323,7 +323,7 @@
    7.13    | SOME (Complex_const_syntax (k, print)) =>
    7.14        let
    7.15          fun print' fxy ts =
    7.16 -          print (print_term some_thm) some_thm vars fxy (ts ~~ take k arg_tys);
    7.17 +          print (print_term some_thm) some_thm vars fxy (ts ~~ take k dom);
    7.18        in
    7.19          if k = length ts
    7.20          then print' fxy ts
     8.1 --- a/src/Tools/Code/code_scala.ML	Mon Jun 04 12:55:54 2012 +0200
     8.2 +++ b/src/Tools/Code/code_scala.ML	Tue Jun 05 07:05:56 2012 +0200
     8.3 @@ -46,8 +46,8 @@
     8.4      fun constraint p1 p2 = Pretty.block [p1, str ":", Pretty.brk 1, p2];
     8.5      fun print_var vars NONE = str "_"
     8.6        | print_var vars (SOME v) = (str o lookup_var vars) v
     8.7 -    fun print_term tyvars is_pat some_thm vars fxy (IConst c) =
     8.8 -          print_app tyvars is_pat some_thm vars fxy (c, [])
     8.9 +    fun print_term tyvars is_pat some_thm vars fxy (IConst const) =
    8.10 +          print_app tyvars is_pat some_thm vars fxy (const, [])
    8.11        | print_term tyvars is_pat some_thm vars fxy (t as (t1 `$ t2)) =
    8.12            (case Code_Thingol.unfold_const_app t
    8.13             of SOME app => print_app tyvars is_pat some_thm vars fxy app
    8.14 @@ -65,30 +65,30 @@
    8.15                print_term tyvars false some_thm vars' NOBR t
    8.16              ]
    8.17            end
    8.18 -      | print_term tyvars is_pat some_thm vars fxy (ICase (cases as (_, t0))) =
    8.19 -          (case Code_Thingol.unfold_const_app t0
    8.20 -           of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
    8.21 -                then print_case tyvars some_thm vars fxy cases
    8.22 -                else print_app tyvars is_pat some_thm vars fxy c_ts
    8.23 -            | NONE => print_case tyvars some_thm vars fxy cases)
    8.24 +      | print_term tyvars is_pat some_thm vars fxy (ICase case_expr) =
    8.25 +          (case Code_Thingol.unfold_const_app (#primitive case_expr)
    8.26 +           of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
    8.27 +                then print_case tyvars some_thm vars fxy case_expr
    8.28 +                else print_app tyvars is_pat some_thm vars fxy app
    8.29 +            | NONE => print_case tyvars some_thm vars fxy case_expr)
    8.30      and print_app tyvars is_pat some_thm vars fxy
    8.31 -        (app as ((c, (((tys, _), (arg_tys, _)), _)), ts)) =
    8.32 +        (app as ({ name = c, typargs, dom, ... }, ts)) =
    8.33        let
    8.34          val k = length ts;
    8.35 -        val tys' = if is_pat orelse
    8.36 -          (is_none (const_syntax c) andalso is_singleton_constr c) then [] else tys;
    8.37 +        val typargs' = if is_pat orelse
    8.38 +          (is_none (const_syntax c) andalso is_singleton_constr c) then [] else typargs;
    8.39          val (l, print') = case const_syntax c
    8.40           of NONE => (args_num c, fn fxy => fn ts => applify "(" ")"
    8.41                (print_term tyvars is_pat some_thm vars NOBR) fxy
    8.42                  (applify "[" "]" (print_typ tyvars NOBR)
    8.43 -                  NOBR ((str o deresolve) c) tys') ts)
    8.44 +                  NOBR ((str o deresolve) c) typargs') ts)
    8.45            | SOME (Plain_const_syntax (k, s)) => (k, fn fxy => fn ts => applify "(" ")"
    8.46                (print_term tyvars is_pat some_thm vars NOBR) fxy
    8.47                  (applify "[" "]" (print_typ tyvars NOBR)
    8.48 -                  NOBR (str s) tys') ts)
    8.49 +                  NOBR (str s) typargs') ts)
    8.50            | SOME (Complex_const_syntax (k, print)) =>
    8.51                (k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
    8.52 -                (ts ~~ take k arg_tys))
    8.53 +                (ts ~~ take k dom))
    8.54        in if k = l then print' fxy ts
    8.55        else if k < l then
    8.56          print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
    8.57 @@ -100,9 +100,11 @@
    8.58        end end
    8.59      and print_bind tyvars some_thm fxy p =
    8.60        gen_print_bind (print_term tyvars true) some_thm fxy p
    8.61 -    and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
    8.62 +    and print_case tyvars some_thm vars fxy { clauses = [], ... } =
    8.63 +          (brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"]
    8.64 +      | print_case tyvars some_thm vars fxy (case_expr as { clauses = [_], ... }) =
    8.65            let
    8.66 -            val (bind :: binds, body) = Code_Thingol.unfold_let (ICase cases);
    8.67 +            val (bind :: binds, body) = Code_Thingol.unfold_let (ICase case_expr);
    8.68              fun print_match_val ((pat, ty), t) vars =
    8.69                vars
    8.70                |> print_bind tyvars some_thm BR pat
    8.71 @@ -123,7 +125,7 @@
    8.72                | insert_seps ((_, p) :: (seps_ps as (sep, _) :: _)) =
    8.73                    (if sep then Pretty.block [p, str ";"] else p) :: insert_seps seps_ps
    8.74            in brackify_block fxy (str "{") (insert_seps all_seps_ps) (str "}") end
    8.75 -      | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
    8.76 +      | print_case tyvars some_thm vars fxy { term = t, typ = ty, clauses = clauses as _ :: _, ... } =
    8.77            let
    8.78              fun print_select (pat, body) =
    8.79                let
    8.80 @@ -135,9 +137,7 @@
    8.81              |> Pretty.block_enclose (concat [print_term tyvars false some_thm vars NOBR t, str "match", str "{"], str "}")
    8.82              |> single
    8.83              |> enclose "(" ")"
    8.84 -          end
    8.85 -      | print_case tyvars some_thm vars fxy ((_, []), _) =
    8.86 -          (brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"];
    8.87 +          end;
    8.88      fun print_context tyvars vs name = applify "[" "]"
    8.89        (fn (v, sort) => (Pretty.block o map str)
    8.90          (lookup_tyvar tyvars v :: maps (fn sort => [" : ", deresolve sort]) sort))
    8.91 @@ -261,19 +261,19 @@
    8.92                :: map print_classparam_def classparams
    8.93              )
    8.94            end
    8.95 -      | print_stmt (name, Code_Thingol.Classinst ((class, (tyco, vs)),
    8.96 -            (super_instances, (classparam_instances, further_classparam_instances)))) =
    8.97 +      | print_stmt (name, Code_Thingol.Classinst
    8.98 +          { class, tyco, vs, inst_params, superinst_params, ... }) =
    8.99            let
   8.100              val tyvars = intro_tyvars vs reserved;
   8.101              val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
   8.102 -            fun print_classparam_instance ((classparam, const as (_, ((_, (tys, _)), _))), (thm, _)) =
   8.103 +            fun print_classparam_instance ((classparam, const as { dom, ... }), (thm, _)) =
   8.104                let
   8.105 -                val aux_tys = Name.invent_names (snd reserved) "a" tys;
   8.106 -                val auxs = map fst aux_tys;
   8.107 +                val aux_dom = Name.invent_names (snd reserved) "a" dom;
   8.108 +                val auxs = map fst aux_dom;
   8.109                  val vars = intro_vars auxs reserved;
   8.110                  val aux_abstr = if null auxs then [] else [enum "," "(" ")"
   8.111                    (map (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
   8.112 -                  (print_typ tyvars NOBR ty)) aux_tys), str "=>"];
   8.113 +                  (print_typ tyvars NOBR ty)) aux_dom), str "=>"];
   8.114                in
   8.115                  concat ([str "val", print_method classparam, str "="]
   8.116                    @ aux_abstr @| print_app tyvars false (SOME thm) vars NOBR
   8.117 @@ -283,7 +283,7 @@
   8.118              Pretty.block_enclose (concat [str "implicit def",
   8.119                constraint (print_context tyvars vs name) (print_dicttyp tyvars classtyp),
   8.120                str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}")
   8.121 -                (map print_classparam_instance (classparam_instances @ further_classparam_instances))
   8.122 +                (map print_classparam_instance (inst_params @ superinst_params))
   8.123            end;
   8.124    in print_stmt end;
   8.125  
     9.1 --- a/src/Tools/Code/code_simp.ML	Mon Jun 04 12:55:54 2012 +0200
     9.2 +++ b/src/Tools/Code/code_simp.ML	Tue Jun 05 07:05:56 2012 +0200
     9.3 @@ -38,8 +38,8 @@
     9.4  fun add_stmt (Code_Thingol.Fun (_, ((_, eqs), some_cong))) ss =
     9.5        ss addsimps (map_filter (fst o snd)) eqs
     9.6        |> fold Simplifier.add_cong (the_list some_cong)
     9.7 -  | add_stmt (Code_Thingol.Classinst (_, (_, (classparam_instances, _)))) ss =
     9.8 -      ss addsimps (map (fst o snd) classparam_instances)
     9.9 +  | add_stmt (Code_Thingol.Classinst { inst_params, ... }) ss =
    9.10 +      ss addsimps (map (fst o snd) inst_params)
    9.11    | add_stmt _ ss = ss;
    9.12  
    9.13  val add_program = Graph.fold (add_stmt o fst o snd);
    10.1 --- a/src/Tools/Code/code_thingol.ML	Mon Jun 04 12:55:54 2012 +0200
    10.2 +++ b/src/Tools/Code/code_thingol.ML	Tue Jun 05 07:05:56 2012 +0200
    10.3 @@ -18,19 +18,18 @@
    10.4        Dict of string list * plain_dict
    10.5    and plain_dict = 
    10.6        Dict_Const of string * dict list list
    10.7 -    | Dict_Var of vname * (int * int)
    10.8 +    | Dict_Var of vname * (int * int);
    10.9    datatype itype =
   10.10        `%% of string * itype list
   10.11      | ITyVar of vname;
   10.12 -  type const = string * (((itype list * dict list list) * (itype list * itype)) * bool)
   10.13 -    (* (f [T1..Tn] {dicts} (_::S1) .. (_::Sm)) :: S =^= (f, ((([T1..Tn], dicts), ([S1..Sm], S)), ambiguous)) *)
   10.14 +  type const = { name: string, typargs: itype list, dicts: dict list list,
   10.15 +    dom: itype list, range: itype, annotate: bool };
   10.16    datatype iterm =
   10.17        IConst of const
   10.18      | IVar of vname option
   10.19      | `$ of iterm * iterm
   10.20      | `|=> of (vname option * itype) * iterm
   10.21 -    | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
   10.22 -        (*((term, type), [(selector pattern, body term )]), primitive term)*)
   10.23 +    | ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm };
   10.24    val `$$ : iterm * iterm list -> iterm;
   10.25    val `|==> : (vname option * itype) list * iterm -> iterm;
   10.26    type typscheme = (vname * sort) list * itype;
   10.27 @@ -77,10 +76,10 @@
   10.28      | Class of class * (vname * ((class * string) list * (string * itype) list))
   10.29      | Classrel of class * class
   10.30      | Classparam of string * class
   10.31 -    | Classinst of (class * (string * (vname * sort) list) (*class and arity*))
   10.32 -          * ((class * (string * (string * dict list list))) list (*super instances*)
   10.33 -        * (((string * const) * (thm * bool)) list (*class parameter instances*)
   10.34 -          * ((string * const) * (thm * bool)) list (*super class parameter instances*)))
   10.35 +    | Classinst of { class: string, tyco: string, vs: (vname * sort) list,
   10.36 +        superinsts: (class * (string * (string * dict list list))) list,
   10.37 +        inst_params: ((string * const) * (thm * bool)) list,
   10.38 +        superinst_params: ((string * const) * (thm * bool)) list };
   10.39    type program = stmt Graph.T
   10.40    val empty_funs: program -> string list
   10.41    val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
   10.42 @@ -126,7 +125,7 @@
   10.43    case dest x
   10.44     of NONE => ([], x)
   10.45      | SOME (x1, x2) =>
   10.46 -        let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end;
   10.47 +        let val (xs', x') = unfoldr dest x2 in (x1 :: xs', x') end;
   10.48  
   10.49  
   10.50  (** language core - types, terms **)
   10.51 @@ -137,21 +136,21 @@
   10.52      Dict of string list * plain_dict
   10.53  and plain_dict = 
   10.54      Dict_Const of string * dict list list
   10.55 -  | Dict_Var of vname * (int * int)
   10.56 +  | Dict_Var of vname * (int * int);
   10.57  
   10.58  datatype itype =
   10.59      `%% of string * itype list
   10.60    | ITyVar of vname;
   10.61  
   10.62 -type const = string * (((itype list * dict list list) *
   10.63 -  (itype list (*types of arguments*) * itype (*result type*))) * bool (*requires type annotation*))
   10.64 +type const = { name: string, typargs: itype list, dicts: dict list list,
   10.65 +  dom: itype list, range: itype, annotate: bool };
   10.66  
   10.67  datatype iterm =
   10.68      IConst of const
   10.69    | IVar of vname option
   10.70    | `$ of iterm * iterm
   10.71    | `|=> of (vname option * itype) * iterm
   10.72 -  | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
   10.73 +  | ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm };
   10.74      (*see also signature*)
   10.75  
   10.76  fun is_IVar (IVar _) = true
   10.77 @@ -172,7 +171,7 @@
   10.78      | _ => NONE);
   10.79  
   10.80  val split_let = 
   10.81 -  (fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t)
   10.82 +  (fn ICase { term = t, typ = ty, clauses = [(p, body)], ... } => SOME (((p, ty), t), body)
   10.83      | _ => NONE);
   10.84  
   10.85  val unfold_let = unfoldr split_let;
   10.86 @@ -188,16 +187,16 @@
   10.87        | fold' (IVar _) = I
   10.88        | fold' (t1 `$ t2) = fold' t1 #> fold' t2
   10.89        | fold' (_ `|=> t) = fold' t
   10.90 -      | fold' (ICase (((t, _), ds), _)) = fold' t
   10.91 -          #> fold (fn (pat, body) => fold' pat #> fold' body) ds
   10.92 +      | fold' (ICase { term = t, clauses = clauses, ... }) = fold' t
   10.93 +          #> fold (fn (p, body) => fold' p #> fold' body) clauses
   10.94    in fold' end;
   10.95  
   10.96 -val add_constnames = fold_constexprs (fn (c, _) => insert (op =) c);
   10.97 +val add_constnames = fold_constexprs (fn { name = c, ... } => insert (op =) c);
   10.98  
   10.99  fun add_tycos (tyco `%% tys) = insert (op =) tyco #> fold add_tycos tys
  10.100    | add_tycos (ITyVar _) = I;
  10.101  
  10.102 -val add_tyconames = fold_constexprs (fn (_, (((tys, _), _), _)) => fold add_tycos tys);
  10.103 +val add_tyconames = fold_constexprs (fn { typargs = tys, ... } => fold add_tycos tys);
  10.104  
  10.105  fun fold_varnames f =
  10.106    let
  10.107 @@ -209,7 +208,7 @@
  10.108            | fold_term vs (t1 `$ t2) = fold_term vs t1 #> fold_term vs t2
  10.109            | fold_term vs ((SOME v, _) `|=> t) = fold_term (insert (op =) v vs) t
  10.110            | fold_term vs ((NONE, _) `|=> t) = fold_term vs t
  10.111 -          | fold_term vs (ICase (((t, _), ds), _)) = fold_term vs t #> fold (fold_case vs) ds
  10.112 +          | fold_term vs (ICase { term = t, clauses = clauses, ... }) = fold_term vs t #> fold (fold_case vs) clauses
  10.113          and fold_case vs (p, t) = fold_term (add p vs) t;
  10.114        in fold_term [] end;
  10.115      fun add t = fold_aux add (insert (op =)) t;
  10.116 @@ -219,9 +218,9 @@
  10.117  
  10.118  fun split_pat_abs ((NONE, ty) `|=> t) = SOME ((IVar NONE, ty), t)
  10.119    | split_pat_abs ((SOME v, ty) `|=> t) = SOME (case t
  10.120 -     of ICase (((IVar (SOME w), _), [(p, t')]), _) =>
  10.121 -          if v = w andalso (exists_var p v orelse not (exists_var t' v))
  10.122 -          then ((p, ty), t')
  10.123 +     of ICase { term = IVar (SOME w), clauses = [(p, body)], ... } =>
  10.124 +          if v = w andalso (exists_var p v orelse not (exists_var body v))
  10.125 +          then ((p, ty), body)
  10.126            else ((IVar (SOME v), ty), t)
  10.127        | _ => ((IVar (SOME v), ty), t))
  10.128    | split_pat_abs _ = NONE;
  10.129 @@ -239,27 +238,27 @@
  10.130          val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys);
  10.131        in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
  10.132  
  10.133 -fun eta_expand k (c as (name, ((_, (tys, _)), _)), ts) =
  10.134 +fun eta_expand k (const as { name = c, dom = tys, ... }, ts) =
  10.135    let
  10.136      val j = length ts;
  10.137      val l = k - j;
  10.138      val _ = if l > length tys
  10.139 -      then error ("Impossible eta-expansion for constant " ^ quote name) else ();
  10.140 +      then error ("Impossible eta-expansion for constant " ^ quote c) else ();
  10.141      val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
  10.142      val vs_tys = (map o apfst) SOME
  10.143        (Name.invent_names ctxt "a" ((take l o drop j) tys));
  10.144 -  in vs_tys `|==> IConst c `$$ ts @ map (IVar o fst) vs_tys end;
  10.145 +  in vs_tys `|==> IConst const `$$ ts @ map (IVar o fst) vs_tys end;
  10.146  
  10.147  fun contains_dict_var t =
  10.148    let
  10.149      fun cont_dict (Dict (_, d)) = cont_plain_dict d
  10.150      and cont_plain_dict (Dict_Const (_, dss)) = (exists o exists) cont_dict dss
  10.151        | cont_plain_dict (Dict_Var _) = true;
  10.152 -    fun cont_term (IConst (_, (((_, dss), _), _))) = (exists o exists) cont_dict dss
  10.153 +    fun cont_term (IConst { dicts = dss, ... }) = (exists o exists) cont_dict dss
  10.154        | cont_term (IVar _) = false
  10.155        | cont_term (t1 `$ t2) = cont_term t1 orelse cont_term t2
  10.156        | cont_term (_ `|=> t) = cont_term t
  10.157 -      | cont_term (ICase (_, t)) = cont_term t;
  10.158 +      | cont_term (ICase { primitive = t, ... }) = cont_term t;
  10.159    in cont_term t end;
  10.160  
  10.161  
  10.162 @@ -427,11 +426,10 @@
  10.163    | Class of class * (vname * ((class * string) list * (string * itype) list))
  10.164    | Classrel of class * class
  10.165    | Classparam of string * class
  10.166 -  | Classinst of (class * (string * (vname * sort) list))
  10.167 -        * ((class * (string * (string * dict list list))) list
  10.168 -      * (((string * const) * (thm * bool)) list
  10.169 -        * ((string * const) * (thm * bool)) list))
  10.170 -      (*see also signature*);
  10.171 +  | Classinst of { class: string, tyco: string, vs: (vname * sort) list,
  10.172 +      superinsts: (class * (string * (string * dict list list))) list,
  10.173 +      inst_params: ((string * const) * (thm * bool)) list,
  10.174 +      superinst_params: ((string * const) * (thm * bool)) list };
  10.175  
  10.176  type program = stmt Graph.T;
  10.177  
  10.178 @@ -444,9 +442,10 @@
  10.179        (map_terms_bottom_up f t1 `$ map_terms_bottom_up f t2)
  10.180    | map_terms_bottom_up f ((v, ty) `|=> t) = f
  10.181        ((v, ty) `|=> map_terms_bottom_up f t)
  10.182 -  | map_terms_bottom_up f (ICase (((t, ty), ps), t0)) = f
  10.183 -      (ICase (((map_terms_bottom_up f t, ty), (map o pairself)
  10.184 -        (map_terms_bottom_up f) ps), map_terms_bottom_up f t0));
  10.185 +  | map_terms_bottom_up f (ICase { term = t, typ = ty, clauses = clauses, primitive = t0 }) = f
  10.186 +      (ICase { term = map_terms_bottom_up f t, typ = ty,
  10.187 +        clauses = (map o pairself) (map_terms_bottom_up f) clauses,
  10.188 +        primitive = map_terms_bottom_up f t0 });
  10.189  
  10.190  fun map_classparam_instances_as_term f =
  10.191    (map o apfst o apsnd) (fn const => case f (IConst const) of IConst const' => const')
  10.192 @@ -459,8 +458,11 @@
  10.193    | map_terms_stmt f (stmt as Class _) = stmt
  10.194    | map_terms_stmt f (stmt as Classrel _) = stmt
  10.195    | map_terms_stmt f (stmt as Classparam _) = stmt
  10.196 -  | map_terms_stmt f (Classinst (arity, (super_instances, classparam_instances))) =
  10.197 -      Classinst (arity, (super_instances, (pairself o map_classparam_instances_as_term) f classparam_instances));
  10.198 +  | map_terms_stmt f (Classinst { class, tyco, vs, superinsts,
  10.199 +      inst_params, superinst_params }) =
  10.200 +        Classinst { class = class, tyco = tyco, vs = vs, superinsts = superinsts,
  10.201 +          inst_params = map_classparam_instances_as_term f inst_params,
  10.202 +          superinst_params = map_classparam_instances_as_term f superinst_params };
  10.203  
  10.204  fun is_cons program name = case Graph.get_node program name
  10.205   of Datatypecons _ => true
  10.206 @@ -484,7 +486,7 @@
  10.207            quote (Proof_Context.extern_class ctxt sub ^ " < " ^ Proof_Context.extern_class ctxt super)
  10.208          end
  10.209      | Classparam (c, _) => quote (Code.string_of_const thy c)
  10.210 -    | Classinst ((class, (tyco, _)), _) =>
  10.211 +    | Classinst { class, tyco, ... } =>
  10.212          let
  10.213            val Class (class, _) = Graph.get_node program class;
  10.214            val Datatype (tyco, _) = Graph.get_node program tyco;
  10.215 @@ -678,9 +680,9 @@
  10.216  and ensure_inst thy (algbr as (_, algebra)) eqngr permissive (class, tyco) =
  10.217    let
  10.218      val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
  10.219 -    val these_classparams = these o try (#params o AxClass.get_info thy);
  10.220 -    val classparams = these_classparams class;
  10.221 -    val further_classparams = maps these_classparams
  10.222 +    val these_class_params = these o try (#params o AxClass.get_info thy);
  10.223 +    val class_params = these_class_params class;
  10.224 +    val superclass_params = maps these_class_params
  10.225        ((Sorts.complete_sort algebra o Sorts.super_classes algebra) class);
  10.226      val vs = Name.invent_names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
  10.227      val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
  10.228 @@ -710,12 +712,11 @@
  10.229        ##>> ensure_tyco thy algbr eqngr permissive tyco
  10.230        ##>> fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
  10.231        ##>> fold_map translate_super_instance super_classes
  10.232 -      ##>> fold_map translate_classparam_instance classparams
  10.233 -      ##>> fold_map translate_classparam_instance further_classparams
  10.234 -      #>> (fn (((((class, tyco), arity_args), super_instances),
  10.235 -        classparam_instances), further_classparam_instances) =>
  10.236 -          Classinst ((class, (tyco, arity_args)), (super_instances,
  10.237 -            (classparam_instances, further_classparam_instances))));
  10.238 +      ##>> fold_map translate_classparam_instance class_params
  10.239 +      ##>> fold_map translate_classparam_instance superclass_params
  10.240 +      #>> (fn (((((class, tyco), vs), superinsts), inst_params), superinst_params) =>
  10.241 +          Classinst { class = class, tyco = tyco, vs = vs,
  10.242 +            superinsts = superinsts, inst_params = inst_params, superinst_params = superinst_params });
  10.243    in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end
  10.244  and translate_typ thy algbr eqngr permissive (TFree (v, _)) =
  10.245        pair (ITyVar (unprefix "'" v))
  10.246 @@ -759,17 +760,18 @@
  10.247          then translation_error thy permissive some_thm
  10.248            "Abstraction violation" ("constant " ^ Code.string_of_const thy c)
  10.249        else ()
  10.250 -    val (annotate, ty') = dest_tagged_type ty
  10.251 -    val arg_typs = Sign.const_typargs thy (c, ty');
  10.252 +    val (annotate, ty') = dest_tagged_type ty;
  10.253 +    val typargs = Sign.const_typargs thy (c, ty');
  10.254      val sorts = Code_Preproc.sortargs eqngr c;
  10.255 -    val (function_typs, body_typ) = Term.strip_type ty';
  10.256 +    val (dom, range) = Term.strip_type ty';
  10.257    in
  10.258      ensure_const thy algbr eqngr permissive c
  10.259 -    ##>> fold_map (translate_typ thy algbr eqngr permissive) arg_typs
  10.260 -    ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (arg_typs ~~ sorts)
  10.261 -    ##>> fold_map (translate_typ thy algbr eqngr permissive) (body_typ :: function_typs)
  10.262 -    #>> (fn (((c, arg_typs), dss), body_typ :: function_typs) =>
  10.263 -      IConst (c, (((arg_typs, dss), (function_typs, body_typ)), annotate)))
  10.264 +    ##>> fold_map (translate_typ thy algbr eqngr permissive) typargs
  10.265 +    ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (typargs ~~ sorts)
  10.266 +    ##>> fold_map (translate_typ thy algbr eqngr permissive) (range :: dom)
  10.267 +    #>> (fn (((c, typargs), dss), range :: dom) =>
  10.268 +      IConst { name = c, typargs = typargs, dicts = dss,
  10.269 +        dom = dom, range = range, annotate = annotate })
  10.270    end
  10.271  and translate_app_const thy algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
  10.272    translate_const thy algbr eqngr permissive some_thm (c_ty, some_abs)
  10.273 @@ -788,22 +790,22 @@
  10.274      val constrs =
  10.275        if null case_pats then []
  10.276        else map_filter I (map2 mk_constr case_pats (nth_drop t_pos ts));
  10.277 -    fun casify naming constrs ty ts =
  10.278 +    fun casify naming constrs ty t_app ts =
  10.279        let
  10.280          val undefineds = map_filter (lookup_const naming) (Code.undefineds thy);
  10.281          fun collapse_clause vs_map ts body =
  10.282            let
  10.283            in case body
  10.284 -           of IConst (c, _) => if member (op =) undefineds c
  10.285 +           of IConst { name = c, ... } => if member (op =) undefineds c
  10.286                  then []
  10.287                  else [(ts, body)]
  10.288 -            | ICase (((IVar (SOME v), _), subclauses), _) =>
  10.289 +            | ICase { term = IVar (SOME v), clauses = clauses, ... } =>
  10.290                  if forall (fn (pat', body') => exists_var pat' v
  10.291 -                  orelse not (exists_var body' v)) subclauses
  10.292 +                  orelse not (exists_var body' v)) clauses
  10.293                  then case AList.lookup (op =) vs_map v
  10.294                   of SOME i => maps (fn (pat', body') =>
  10.295                        collapse_clause (AList.delete (op =) v vs_map)
  10.296 -                        (nth_map i (K pat') ts) body') subclauses
  10.297 +                        (nth_map i (K pat') ts) body') clauses
  10.298                    | NONE => [(ts, body)]
  10.299                  else [(ts, body)]
  10.300              | _ => [(ts, body)]
  10.301 @@ -818,11 +820,11 @@
  10.302          val ts_clause = nth_drop t_pos ts;
  10.303          val clauses = if null case_pats
  10.304            then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause)
  10.305 -          else maps (fn ((constr as IConst (_, ((_, (tys, _)), _)), n), t) =>
  10.306 +          else maps (fn ((constr as IConst { dom = tys, ... }, n), t) =>
  10.307              mk_clause (fn (ts, body) => (constr `$$ ts, body)) (take n tys) t)
  10.308                (constrs ~~ (map_filter (fn (NONE, _) => NONE | (SOME _, t) => SOME t)
  10.309                  (case_pats ~~ ts_clause)));
  10.310 -      in ((t, ty), clauses) end;
  10.311 +      in ICase { term = t, typ = ty, clauses = clauses, primitive = t_app `$$ ts } end;
  10.312    in
  10.313      translate_const thy algbr eqngr permissive some_thm (c_ty, NONE)
  10.314      ##>> fold_map (fn (constr, n) => translate_const thy algbr eqngr permissive some_thm (constr, NONE)
  10.315 @@ -830,7 +832,7 @@
  10.316      ##>> translate_typ thy algbr eqngr permissive ty
  10.317      ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts
  10.318      #-> (fn (((t, constrs), ty), ts) =>
  10.319 -      `(fn (_, (naming, _)) => ICase (casify naming constrs ty ts, t `$$ ts)))
  10.320 +      `(fn (_, (naming, _)) => casify naming constrs ty t ts))
  10.321    end
  10.322  and translate_app_case thy algbr eqngr permissive some_thm (case_scheme as (num_args, _)) ((c, ty), ts) =
  10.323    if length ts < num_args then
    11.1 --- a/src/Tools/nbe.ML	Mon Jun 04 12:55:54 2012 +0200
    11.2 +++ b/src/Tools/nbe.ML	Tue Jun 05 07:05:56 2012 +0200
    11.3 @@ -314,13 +314,13 @@
    11.4            let
    11.5              val (t', ts) = Code_Thingol.unfold_app t
    11.6            in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end
    11.7 -        and of_iapp match_cont (IConst (c, (((_, dss), _), _))) ts = constapp c dss ts
    11.8 +        and of_iapp match_cont (IConst { name = c, dicts = dss, ... }) ts = constapp c dss ts
    11.9            | of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound_optional v) ts
   11.10            | of_iapp match_cont ((v, _) `|=> t) ts =
   11.11                nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound_optional v]) (of_iterm NONE t))) ts
   11.12 -          | of_iapp match_cont (ICase (((t, _), cs), t0)) ts =
   11.13 +          | of_iapp match_cont (ICase { term = t, clauses = clauses, primitive = t0, ... }) ts =
   11.14                nbe_apps (ml_cases (of_iterm NONE t)
   11.15 -                (map (fn (p, t) => (of_iterm NONE p, of_iterm match_cont t)) cs
   11.16 +                (map (fn (p, t) => (of_iterm NONE p, of_iterm match_cont t)) clauses
   11.17                    @ [("_", case match_cont of SOME s => s | NONE => of_iterm NONE t0)])) ts
   11.18        in of_iterm end;
   11.19  
   11.20 @@ -345,7 +345,7 @@
   11.21                |> subst_vars t1
   11.22                ||>> subst_vars t2
   11.23                |>> (op `$)
   11.24 -          | subst_vars (ICase (_, t)) samepairs = subst_vars t samepairs;
   11.25 +          | subst_vars (ICase { primitive = t, ... }) samepairs = subst_vars t samepairs;
   11.26          val (args', _) = fold_map subst_vars args samepairs;
   11.27        in (samepairs, args') end;
   11.28  
   11.29 @@ -410,6 +410,10 @@
   11.30  
   11.31  (* extract equations from statements *)
   11.32  
   11.33 +fun dummy_const c dss =
   11.34 +  IConst { name = c, typargs = [], dicts = dss,
   11.35 +    dom = [], range = ITyVar "", annotate = false };
   11.36 +
   11.37  fun eqns_of_stmt (_, Code_Thingol.Fun (_, ((_, []), _))) =
   11.38        []
   11.39    | eqns_of_stmt (const, Code_Thingol.Fun (_, (((vs, _), eqns), _))) =
   11.40 @@ -424,17 +428,17 @@
   11.41          val params = Name.invent Name.context "d" (length names);
   11.42          fun mk (k, name) =
   11.43            (name, ([(v, [])],
   11.44 -            [([IConst (class, ((([], []), ([], ITyVar "")), false)) `$$ map (IVar o SOME) params],
   11.45 +            [([dummy_const class [] `$$ map (IVar o SOME) params],
   11.46                IVar (SOME (nth params k)))]));
   11.47        in map_index mk names end
   11.48    | eqns_of_stmt (_, Code_Thingol.Classrel _) =
   11.49        []
   11.50    | eqns_of_stmt (_, Code_Thingol.Classparam _) =
   11.51        []
   11.52 -  | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), (super_instances, (classparam_instances, _)))) =
   11.53 -      [(inst, (arity_args, [([], IConst (class, ((([], []), ([], ITyVar "")), false)) `$$
   11.54 -        map (fn (_, (_, (inst, dss))) => IConst (inst, ((([], dss), ([], ITyVar "")), false))) super_instances
   11.55 -        @ map (IConst o snd o fst) classparam_instances)]))];
   11.56 +  | eqns_of_stmt (inst, Code_Thingol.Classinst { class, vs, superinsts, inst_params, ... }) =
   11.57 +      [(inst, (vs, [([], dummy_const class [] `$$
   11.58 +        map (fn (_, (_, (inst, dss))) => dummy_const inst dss) superinsts
   11.59 +        @ map (IConst o snd o fst) inst_params)]))];
   11.60  
   11.61  
   11.62  (* compile whole programs *)