context theorem is optional
authorhaftmann
Fri Feb 19 11:06:22 2010 +0100 (2010-02-19)
changeset 35228ac2cab4583f4
parent 35227 d67857e3a8c0
child 35229 d4ec25836a78
child 35264 f44ef0e2d178
context theorem is optional
src/Tools/Code/code_eval.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
     1.1 --- a/src/Tools/Code/code_eval.ML	Fri Feb 19 11:06:22 2010 +0100
     1.2 +++ b/src/Tools/Code/code_eval.ML	Fri Feb 19 11:06:22 2010 +0100
     1.3 @@ -53,7 +53,7 @@
     1.4          val value_name = "Value.VALUE.value"
     1.5          val program' = program
     1.6            |> Graph.new_node (value_name,
     1.7 -              Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (Drule.dummy_thm, true))])))
     1.8 +              Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (NONE, true))])))
     1.9            |> fold (curry Graph.add_edge value_name) deps;
    1.10          val (value_code, [SOME value_name']) = Code_ML.evaluation_code_of thy
    1.11            (the_default target some_target) "" naming program' [value_name];
     2.1 --- a/src/Tools/Code/code_haskell.ML	Fri Feb 19 11:06:22 2010 +0100
     2.2 +++ b/src/Tools/Code/code_haskell.ML	Fri Feb 19 11:06:22 2010 +0100
     2.3 @@ -50,71 +50,71 @@
     2.4        Pretty.block (print_typcontext tyvars vs @| print_tyco_expr tyvars NOBR tycoexpr);
     2.5      fun print_typscheme tyvars (vs, ty) =
     2.6        Pretty.block (print_typforall tyvars vs @ print_typcontext tyvars vs @| print_typ tyvars NOBR ty);
     2.7 -    fun print_term tyvars thm vars fxy (IConst c) =
     2.8 -          print_app tyvars thm vars fxy (c, [])
     2.9 -      | print_term tyvars thm vars fxy (t as (t1 `$ t2)) =
    2.10 +    fun print_term tyvars some_thm vars fxy (IConst c) =
    2.11 +          print_app tyvars some_thm vars fxy (c, [])
    2.12 +      | print_term tyvars some_thm vars fxy (t as (t1 `$ t2)) =
    2.13            (case Code_Thingol.unfold_const_app t
    2.14 -           of SOME app => print_app tyvars thm vars fxy app
    2.15 +           of SOME app => print_app tyvars some_thm vars fxy app
    2.16              | _ =>
    2.17                  brackify fxy [
    2.18 -                  print_term tyvars thm vars NOBR t1,
    2.19 -                  print_term tyvars thm vars BR t2
    2.20 +                  print_term tyvars some_thm vars NOBR t1,
    2.21 +                  print_term tyvars some_thm vars BR t2
    2.22                  ])
    2.23 -      | print_term tyvars thm vars fxy (IVar NONE) =
    2.24 +      | print_term tyvars some_thm vars fxy (IVar NONE) =
    2.25            str "_"
    2.26 -      | print_term tyvars thm vars fxy (IVar (SOME v)) =
    2.27 +      | print_term tyvars some_thm vars fxy (IVar (SOME v)) =
    2.28            (str o lookup_var vars) v
    2.29 -      | print_term tyvars thm vars fxy (t as _ `|=> _) =
    2.30 +      | print_term tyvars some_thm vars fxy (t as _ `|=> _) =
    2.31            let
    2.32              val (binds, t') = Code_Thingol.unfold_pat_abs t;
    2.33 -            val (ps, vars') = fold_map (print_bind tyvars thm BR o fst) binds vars;
    2.34 -          in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars thm vars' NOBR t') end
    2.35 -      | print_term tyvars thm vars fxy (ICase (cases as (_, t0))) =
    2.36 +            val (ps, vars') = fold_map (print_bind tyvars some_thm BR o fst) binds vars;
    2.37 +          in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end
    2.38 +      | print_term tyvars some_thm vars fxy (ICase (cases as (_, t0))) =
    2.39            (case Code_Thingol.unfold_const_app t0
    2.40             of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
    2.41 -                then print_case tyvars thm vars fxy cases
    2.42 -                else print_app tyvars thm vars fxy c_ts
    2.43 -            | NONE => print_case tyvars thm vars fxy cases)
    2.44 -    and print_app_expr tyvars thm vars ((c, (_, tys)), ts) = case contr_classparam_typs c
    2.45 -     of [] => (str o deresolve) c :: map (print_term tyvars thm vars BR) ts
    2.46 +                then print_case tyvars some_thm vars fxy cases
    2.47 +                else print_app tyvars some_thm vars fxy c_ts
    2.48 +            | NONE => print_case tyvars some_thm vars fxy cases)
    2.49 +    and print_app_expr tyvars some_thm vars ((c, (_, tys)), ts) = case contr_classparam_typs c
    2.50 +     of [] => (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts
    2.51        | fingerprint => let
    2.52            val ts_fingerprint = ts ~~ take (length ts) fingerprint;
    2.53            val needs_annotation = forall (fn (_, NONE) => true | (t, SOME _) =>
    2.54              (not o Code_Thingol.locally_monomorphic) t) ts_fingerprint;
    2.55 -          fun print_term_anno (t, NONE) _ = print_term tyvars thm vars BR t
    2.56 +          fun print_term_anno (t, NONE) _ = print_term tyvars some_thm vars BR t
    2.57              | print_term_anno (t, SOME _) ty =
    2.58 -                brackets [print_term tyvars thm vars NOBR t, str "::", print_typ tyvars NOBR ty];
    2.59 +                brackets [print_term tyvars some_thm vars NOBR t, str "::", print_typ tyvars NOBR ty];
    2.60          in
    2.61            if needs_annotation then
    2.62              (str o deresolve) c :: map2 print_term_anno ts_fingerprint (take (length ts) tys)
    2.63 -          else (str o deresolve) c :: map (print_term tyvars thm vars BR) ts
    2.64 +          else (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts
    2.65          end
    2.66      and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) syntax_const
    2.67 -    and print_bind tyvars thm fxy p = gen_print_bind (print_term tyvars) thm fxy p
    2.68 -    and print_case tyvars thm vars fxy (cases as ((_, [_]), _)) =
    2.69 +    and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
    2.70 +    and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
    2.71            let
    2.72              val (binds, body) = Code_Thingol.unfold_let (ICase cases);
    2.73              fun print_match ((pat, ty), t) vars =
    2.74                vars
    2.75 -              |> print_bind tyvars thm BR pat
    2.76 -              |>> (fn p => semicolon [p, str "=", print_term tyvars thm vars NOBR t])
    2.77 +              |> print_bind tyvars some_thm BR pat
    2.78 +              |>> (fn p => semicolon [p, str "=", print_term tyvars some_thm vars NOBR t])
    2.79              val (ps, vars') = fold_map print_match binds vars;
    2.80            in brackify_block fxy (str "let {")
    2.81              ps
    2.82 -            (concat [str "}", str "in", print_term tyvars thm vars' NOBR body])
    2.83 +            (concat [str "}", str "in", print_term tyvars some_thm vars' NOBR body])
    2.84            end
    2.85 -      | print_case tyvars thm vars fxy (((t, ty), clauses as _ :: _), _) =
    2.86 +      | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
    2.87            let
    2.88              fun print_select (pat, body) =
    2.89                let
    2.90 -                val (p, vars') = print_bind tyvars thm NOBR pat vars;
    2.91 -              in semicolon [p, str "->", print_term tyvars thm vars' NOBR body] end;
    2.92 +                val (p, vars') = print_bind tyvars some_thm NOBR pat vars;
    2.93 +              in semicolon [p, str "->", print_term tyvars some_thm vars' NOBR body] end;
    2.94            in brackify_block fxy
    2.95 -            (concat [str "case", print_term tyvars thm vars NOBR t, str "of", str "{"])
    2.96 +            (concat [str "case", print_term tyvars some_thm vars NOBR t, str "of", str "{"])
    2.97              (map print_select clauses)
    2.98              (str "}") 
    2.99            end
   2.100 -      | print_case tyvars thm vars fxy ((_, []), _) =
   2.101 +      | print_case tyvars some_thm vars fxy ((_, []), _) =
   2.102            (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
   2.103      fun print_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) =
   2.104            let
   2.105 @@ -128,7 +128,7 @@
   2.106                  @@ (str o ML_Syntax.print_string
   2.107                      o Long_Name.base_name o Long_Name.qualifier) name
   2.108                );
   2.109 -            fun print_eqn ((ts, t), (thm, _)) =
   2.110 +            fun print_eqn ((ts, t), (some_thm, _)) =
   2.111                let
   2.112                  val consts = fold Code_Thingol.add_constnames (t :: ts) [];
   2.113                  val vars = reserved
   2.114 @@ -139,9 +139,9 @@
   2.115                in
   2.116                  semicolon (
   2.117                    (str o deresolve_base) name
   2.118 -                  :: map (print_term tyvars thm vars BR) ts
   2.119 +                  :: map (print_term tyvars some_thm vars BR) ts
   2.120                    @ str "="
   2.121 -                  @@ print_term tyvars thm vars NOBR t
   2.122 +                  @@ print_term tyvars some_thm vars NOBR t
   2.123                  )
   2.124                end;
   2.125            in
   2.126 @@ -222,7 +222,7 @@
   2.127               of NONE => semicolon [
   2.128                      (str o deresolve_base) classparam,
   2.129                      str "=",
   2.130 -                    print_app tyvars thm reserved NOBR (c_inst, [])
   2.131 +                    print_app tyvars (SOME thm) reserved NOBR (c_inst, [])
   2.132                    ]
   2.133                | SOME (k, pr) =>
   2.134                    let
   2.135 @@ -238,9 +238,9 @@
   2.136                        (*dictionaries are not relevant at this late stage*)
   2.137                    in
   2.138                      semicolon [
   2.139 -                      print_term tyvars thm vars NOBR lhs,
   2.140 +                      print_term tyvars (SOME thm) vars NOBR lhs,
   2.141                        str "=",
   2.142 -                      print_term tyvars thm vars NOBR rhs
   2.143 +                      print_term tyvars (SOME thm) vars NOBR rhs
   2.144                      ]
   2.145                    end;
   2.146            in
     3.1 --- a/src/Tools/Code/code_ml.ML	Fri Feb 19 11:06:22 2010 +0100
     3.2 +++ b/src/Tools/Code/code_ml.ML	Fri Feb 19 11:06:22 2010 +0100
     3.3 @@ -28,7 +28,7 @@
     3.4  val target_OCaml = "OCaml";
     3.5  
     3.6  datatype ml_binding =
     3.7 -    ML_Function of string * (typscheme * ((iterm list * iterm) * (thm * bool)) list)
     3.8 +    ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
     3.9    | ML_Instance of string * ((class * (string * (vname * sort) list))
    3.10          * ((class * (string * (string * dict list list))) list
    3.11        * ((string * const) * (thm * bool)) list));
    3.12 @@ -94,79 +94,79 @@
    3.13      and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun);
    3.14      val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
    3.15        (map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort));
    3.16 -    fun print_term is_pseudo_fun thm vars fxy (IConst c) =
    3.17 -          print_app is_pseudo_fun thm vars fxy (c, [])
    3.18 -      | print_term is_pseudo_fun thm vars fxy (IVar NONE) =
    3.19 +    fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
    3.20 +          print_app is_pseudo_fun some_thm vars fxy (c, [])
    3.21 +      | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
    3.22            str "_"
    3.23 -      | print_term is_pseudo_fun thm vars fxy (IVar (SOME v)) =
    3.24 +      | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =
    3.25            str (lookup_var vars v)
    3.26 -      | print_term is_pseudo_fun thm vars fxy (t as t1 `$ t2) =
    3.27 +      | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =
    3.28            (case Code_Thingol.unfold_const_app t
    3.29 -           of SOME c_ts => print_app is_pseudo_fun thm vars fxy c_ts
    3.30 -            | NONE => brackify fxy [print_term is_pseudo_fun thm vars NOBR t1,
    3.31 -                print_term is_pseudo_fun thm vars BR t2])
    3.32 -      | print_term is_pseudo_fun thm vars fxy (t as _ `|=> _) =
    3.33 +           of SOME c_ts => print_app is_pseudo_fun some_thm vars fxy c_ts
    3.34 +            | NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1,
    3.35 +                print_term is_pseudo_fun some_thm vars BR t2])
    3.36 +      | print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) =
    3.37            let
    3.38              val (binds, t') = Code_Thingol.unfold_pat_abs t;
    3.39              fun print_abs (pat, ty) =
    3.40 -              print_bind is_pseudo_fun thm NOBR pat
    3.41 +              print_bind is_pseudo_fun some_thm NOBR pat
    3.42                #>> (fn p => concat [str "fn", p, str "=>"]);
    3.43              val (ps, vars') = fold_map print_abs binds vars;
    3.44 -          in brackets (ps @ [print_term is_pseudo_fun thm vars' NOBR t']) end
    3.45 -      | print_term is_pseudo_fun thm vars fxy (ICase (cases as (_, t0))) =
    3.46 +          in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end
    3.47 +      | print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =
    3.48            (case Code_Thingol.unfold_const_app t0
    3.49             of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
    3.50 -                then print_case is_pseudo_fun thm vars fxy cases
    3.51 -                else print_app is_pseudo_fun thm vars fxy c_ts
    3.52 -            | NONE => print_case is_pseudo_fun thm vars fxy cases)
    3.53 -    and print_app_expr is_pseudo_fun thm vars (app as ((c, ((_, iss), tys)), ts)) =
    3.54 +                then print_case is_pseudo_fun some_thm vars fxy cases
    3.55 +                else print_app is_pseudo_fun some_thm vars fxy c_ts
    3.56 +            | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
    3.57 +    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), tys)), ts)) =
    3.58        if is_cons c then
    3.59          let val k = length tys in
    3.60            if k < 2 orelse length ts = k
    3.61            then (str o deresolve) c
    3.62 -            :: the_list (print_tuple (print_term is_pseudo_fun thm vars) BR ts)
    3.63 -          else [print_term is_pseudo_fun thm vars BR (Code_Thingol.eta_expand k app)]
    3.64 +            :: the_list (print_tuple (print_term is_pseudo_fun some_thm vars) BR ts)
    3.65 +          else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
    3.66          end
    3.67        else if is_pseudo_fun c
    3.68          then (str o deresolve) c @@ str "()"
    3.69        else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
    3.70 -        @ map (print_term is_pseudo_fun thm vars BR) ts
    3.71 -    and print_app is_pseudo_fun thm vars = gen_print_app (print_app_expr is_pseudo_fun)
    3.72 -      (print_term is_pseudo_fun) syntax_const thm vars
    3.73 +        @ map (print_term is_pseudo_fun some_thm vars BR) ts
    3.74 +    and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
    3.75 +      (print_term is_pseudo_fun) syntax_const some_thm vars
    3.76      and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
    3.77 -    and print_case is_pseudo_fun thm vars fxy (cases as ((_, [_]), _)) =
    3.78 +    and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
    3.79            let
    3.80              val (binds, body) = Code_Thingol.unfold_let (ICase cases);
    3.81              fun print_match ((pat, ty), t) vars =
    3.82                vars
    3.83 -              |> print_bind is_pseudo_fun thm NOBR pat
    3.84 +              |> print_bind is_pseudo_fun some_thm NOBR pat
    3.85                |>> (fn p => semicolon [str "val", p, str "=",
    3.86 -                    print_term is_pseudo_fun thm vars NOBR t])
    3.87 +                    print_term is_pseudo_fun some_thm vars NOBR t])
    3.88              val (ps, vars') = fold_map print_match binds vars;
    3.89            in
    3.90              Pretty.chunks [
    3.91                Pretty.block [str "let", Pretty.fbrk, Pretty.chunks ps],
    3.92 -              Pretty.block [str "in", Pretty.fbrk, print_term is_pseudo_fun thm vars' NOBR body],
    3.93 +              Pretty.block [str "in", Pretty.fbrk, print_term is_pseudo_fun some_thm vars' NOBR body],
    3.94                str "end"
    3.95              ]
    3.96            end
    3.97 -      | print_case is_pseudo_fun thm vars fxy (((t, ty), clause :: clauses), _) =
    3.98 +      | print_case is_pseudo_fun some_thm vars fxy (((t, ty), clause :: clauses), _) =
    3.99            let
   3.100              fun print_select delim (pat, body) =
   3.101                let
   3.102 -                val (p, vars') = print_bind is_pseudo_fun thm NOBR pat vars;
   3.103 +                val (p, vars') = print_bind is_pseudo_fun some_thm NOBR pat vars;
   3.104                in
   3.105 -                concat [str delim, p, str "=>", print_term is_pseudo_fun thm vars' NOBR body]
   3.106 +                concat [str delim, p, str "=>", print_term is_pseudo_fun some_thm vars' NOBR body]
   3.107                end;
   3.108            in
   3.109              brackets (
   3.110                str "case"
   3.111 -              :: print_term is_pseudo_fun thm vars NOBR t
   3.112 +              :: print_term is_pseudo_fun some_thm vars NOBR t
   3.113                :: print_select "of" clause
   3.114                :: map (print_select "|") clauses
   3.115              )
   3.116            end
   3.117 -      | print_case is_pseudo_fun thm vars fxy ((_, []), _) =
   3.118 +      | print_case is_pseudo_fun some_thm vars fxy ((_, []), _) =
   3.119            (concat o map str) ["raise", "Fail", "\"empty case\""];
   3.120      fun print_val_decl print_typscheme (name, typscheme) = concat
   3.121        [str "val", str (deresolve name), str ":", print_typscheme typscheme];
   3.122 @@ -186,7 +186,7 @@
   3.123      fun print_def is_pseudo_fun needs_typ definer
   3.124            (ML_Function (name, (vs_ty as (vs, ty), eq :: eqs))) =
   3.125            let
   3.126 -            fun print_eqn definer ((ts, t), (thm, _)) =
   3.127 +            fun print_eqn definer ((ts, t), (some_thm, _)) =
   3.128                let
   3.129                  val consts = fold Code_Thingol.add_constnames (t :: ts) [];
   3.130                  val vars = reserved
   3.131 @@ -202,9 +202,9 @@
   3.132                    prolog
   3.133                    :: (if is_pseudo_fun name then [str "()"]
   3.134                        else print_dict_args vs
   3.135 -                        @ map (print_term is_pseudo_fun thm vars BR) ts)
   3.136 +                        @ map (print_term is_pseudo_fun some_thm vars BR) ts)
   3.137                    @ str "="
   3.138 -                  @@ print_term is_pseudo_fun thm vars NOBR t
   3.139 +                  @@ print_term is_pseudo_fun some_thm vars NOBR t
   3.140                  )
   3.141                end
   3.142              val shift = if null eqs then I else
   3.143 @@ -229,7 +229,7 @@
   3.144                concat [
   3.145                  (str o Long_Name.base_name o deresolve) classparam,
   3.146                  str "=",
   3.147 -                print_app (K false) thm reserved NOBR (c_inst, [])
   3.148 +                print_app (K false) (SOME thm) reserved NOBR (c_inst, [])
   3.149                ];
   3.150            in pair
   3.151              (print_val_decl print_dicttypscheme
   3.152 @@ -393,71 +393,71 @@
   3.153      and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun);
   3.154      val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
   3.155        (map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort));
   3.156 -    fun print_term is_pseudo_fun thm vars fxy (IConst c) =
   3.157 -          print_app is_pseudo_fun thm vars fxy (c, [])
   3.158 -      | print_term is_pseudo_fun thm vars fxy (IVar NONE) =
   3.159 +    fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
   3.160 +          print_app is_pseudo_fun some_thm vars fxy (c, [])
   3.161 +      | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
   3.162            str "_"
   3.163 -      | print_term is_pseudo_fun thm vars fxy (IVar (SOME v)) =
   3.164 +      | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =
   3.165            str (lookup_var vars v)
   3.166 -      | print_term is_pseudo_fun thm vars fxy (t as t1 `$ t2) =
   3.167 +      | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =
   3.168            (case Code_Thingol.unfold_const_app t
   3.169 -           of SOME c_ts => print_app is_pseudo_fun thm vars fxy c_ts
   3.170 -            | NONE => brackify fxy [print_term is_pseudo_fun thm vars NOBR t1,
   3.171 -                print_term is_pseudo_fun thm vars BR t2])
   3.172 -      | print_term is_pseudo_fun thm vars fxy (t as _ `|=> _) =
   3.173 +           of SOME c_ts => print_app is_pseudo_fun some_thm vars fxy c_ts
   3.174 +            | NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1,
   3.175 +                print_term is_pseudo_fun some_thm vars BR t2])
   3.176 +      | print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) =
   3.177            let
   3.178              val (binds, t') = Code_Thingol.unfold_pat_abs t;
   3.179 -            val (ps, vars') = fold_map (print_bind is_pseudo_fun thm BR o fst) binds vars;
   3.180 -          in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun thm vars' NOBR t') end
   3.181 -      | print_term is_pseudo_fun thm vars fxy (ICase (cases as (_, t0))) =
   3.182 +            val (ps, vars') = fold_map (print_bind is_pseudo_fun some_thm BR o fst) binds vars;
   3.183 +          in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end
   3.184 +      | print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =
   3.185            (case Code_Thingol.unfold_const_app t0
   3.186             of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
   3.187 -                then print_case is_pseudo_fun thm vars fxy cases
   3.188 -                else print_app is_pseudo_fun thm vars fxy c_ts
   3.189 -            | NONE => print_case is_pseudo_fun thm vars fxy cases)
   3.190 -    and print_app_expr is_pseudo_fun thm vars (app as ((c, ((_, iss), tys)), ts)) =
   3.191 +                then print_case is_pseudo_fun some_thm vars fxy cases
   3.192 +                else print_app is_pseudo_fun some_thm vars fxy c_ts
   3.193 +            | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
   3.194 +    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), tys)), ts)) =
   3.195        if is_cons c then
   3.196          let val k = length tys in
   3.197            if length ts = k
   3.198            then (str o deresolve) c
   3.199 -            :: the_list (print_tuple (print_term is_pseudo_fun thm vars) BR ts)
   3.200 -          else [print_term is_pseudo_fun thm vars BR (Code_Thingol.eta_expand k app)]
   3.201 +            :: the_list (print_tuple (print_term is_pseudo_fun some_thm vars) BR ts)
   3.202 +          else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
   3.203          end
   3.204        else if is_pseudo_fun c
   3.205          then (str o deresolve) c @@ str "()"
   3.206        else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
   3.207 -        @ map (print_term is_pseudo_fun thm vars BR) ts
   3.208 -    and print_app is_pseudo_fun thm vars = gen_print_app (print_app_expr is_pseudo_fun)
   3.209 -      (print_term is_pseudo_fun) syntax_const thm vars
   3.210 +        @ map (print_term is_pseudo_fun some_thm vars BR) ts
   3.211 +    and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
   3.212 +      (print_term is_pseudo_fun) syntax_const some_thm vars
   3.213      and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
   3.214 -    and print_case is_pseudo_fun thm vars fxy (cases as ((_, [_]), _)) =
   3.215 +    and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
   3.216            let
   3.217              val (binds, body) = Code_Thingol.unfold_let (ICase cases);
   3.218              fun print_let ((pat, ty), t) vars =
   3.219                vars
   3.220 -              |> print_bind is_pseudo_fun thm NOBR pat
   3.221 +              |> print_bind is_pseudo_fun some_thm NOBR pat
   3.222                |>> (fn p => concat
   3.223 -                  [str "let", p, str "=", print_term is_pseudo_fun thm vars NOBR t, str "in"])
   3.224 +                  [str "let", p, str "=", print_term is_pseudo_fun some_thm vars NOBR t, str "in"])
   3.225              val (ps, vars') = fold_map print_let binds vars;
   3.226            in
   3.227              brackify_block fxy (Pretty.chunks ps) []
   3.228 -              (print_term is_pseudo_fun thm vars' NOBR body)
   3.229 +              (print_term is_pseudo_fun some_thm vars' NOBR body)
   3.230            end
   3.231 -      | print_case is_pseudo_fun thm vars fxy (((t, ty), clause :: clauses), _) =
   3.232 +      | print_case is_pseudo_fun some_thm vars fxy (((t, ty), clause :: clauses), _) =
   3.233            let
   3.234              fun print_select delim (pat, body) =
   3.235                let
   3.236 -                val (p, vars') = print_bind is_pseudo_fun thm NOBR pat vars;
   3.237 -              in concat [str delim, p, str "->", print_term is_pseudo_fun thm vars' NOBR body] end;
   3.238 +                val (p, vars') = print_bind is_pseudo_fun some_thm NOBR pat vars;
   3.239 +              in concat [str delim, p, str "->", print_term is_pseudo_fun some_thm vars' NOBR body] end;
   3.240            in
   3.241              brackets (
   3.242                str "match"
   3.243 -              :: print_term is_pseudo_fun thm vars NOBR t
   3.244 +              :: print_term is_pseudo_fun some_thm vars NOBR t
   3.245                :: print_select "with" clause
   3.246                :: map (print_select "|") clauses
   3.247              )
   3.248            end
   3.249 -      | print_case is_pseudo_fun thm vars fxy ((_, []), _) =
   3.250 +      | print_case is_pseudo_fun some_thm vars fxy ((_, []), _) =
   3.251            (concat o map str) ["failwith", "\"empty case\""];
   3.252      fun print_val_decl print_typscheme (name, typscheme) = concat
   3.253        [str "val", str (deresolve name), str ":", print_typscheme typscheme];
   3.254 @@ -477,7 +477,7 @@
   3.255      fun print_def is_pseudo_fun needs_typ definer
   3.256            (ML_Function (name, (vs_ty as (vs, ty), eqs))) =
   3.257            let
   3.258 -            fun print_eqn ((ts, t), (thm, _)) =
   3.259 +            fun print_eqn ((ts, t), (some_thm, _)) =
   3.260                let
   3.261                  val consts = fold Code_Thingol.add_constnames (t :: ts) [];
   3.262                  val vars = reserved
   3.263 @@ -485,11 +485,11 @@
   3.264                        (insert (op =)) ts []);
   3.265                in concat [
   3.266                  (Pretty.block o Pretty.commas)
   3.267 -                  (map (print_term is_pseudo_fun thm vars NOBR) ts),
   3.268 +                  (map (print_term is_pseudo_fun some_thm vars NOBR) ts),
   3.269                  str "->",
   3.270 -                print_term is_pseudo_fun thm vars NOBR t
   3.271 +                print_term is_pseudo_fun some_thm vars NOBR t
   3.272                ] end;
   3.273 -            fun print_eqns is_pseudo [((ts, t), (thm, _))] =
   3.274 +            fun print_eqns is_pseudo [((ts, t), (some_thm, _))] =
   3.275                    let
   3.276                      val consts = fold Code_Thingol.add_constnames (t :: ts) [];
   3.277                      val vars = reserved
   3.278 @@ -500,9 +500,9 @@
   3.279                    in
   3.280                      concat (
   3.281                        (if is_pseudo then [str "()"]
   3.282 -                        else map (print_term is_pseudo_fun thm vars BR) ts)
   3.283 +                        else map (print_term is_pseudo_fun some_thm vars BR) ts)
   3.284                        @ str "="
   3.285 -                      @@ print_term is_pseudo_fun thm vars NOBR t
   3.286 +                      @@ print_term is_pseudo_fun some_thm vars NOBR t
   3.287                      )
   3.288                    end
   3.289                | print_eqns _ ((eq as (([_], _), _)) :: eqs) =
   3.290 @@ -562,7 +562,7 @@
   3.291                concat [
   3.292                  (str o deresolve) classparam,
   3.293                  str "=",
   3.294 -                print_app (K false) thm reserved NOBR (c_inst, [])
   3.295 +                print_app (K false) (SOME thm) reserved NOBR (c_inst, [])
   3.296                ];
   3.297            in pair
   3.298              (print_val_decl print_dicttypscheme
   3.299 @@ -758,8 +758,8 @@
   3.300            let
   3.301              val eqs = filter (snd o snd) raw_eqs;
   3.302              val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs
   3.303 -               of [(([], t), thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
   3.304 -                  then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), thm)], NONE)
   3.305 +               of [(([], t), some_thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
   3.306 +                  then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), some_thm)], NONE)
   3.307                    else (eqs, SOME (name, member (op =) (Code_Thingol.add_constnames t []) name))
   3.308                  | _ => (eqs, NONE)
   3.309                else (eqs, NONE)
     4.1 --- a/src/Tools/Code/code_printer.ML	Fri Feb 19 11:06:22 2010 +0100
     4.2 +++ b/src/Tools/Code/code_printer.ML	Fri Feb 19 11:06:22 2010 +0100
     4.3 @@ -11,7 +11,7 @@
     4.4    type const = Code_Thingol.const
     4.5    type dict = Code_Thingol.dict
     4.6  
     4.7 -  val eqn_error: thm -> string -> 'a
     4.8 +  val eqn_error: thm option -> string -> 'a
     4.9  
    4.10    val @@ : 'a * 'a -> 'a list
    4.11    val @| : 'a list * 'a -> 'a list
    4.12 @@ -78,12 +78,12 @@
    4.13    val simple_const_syntax: simple_const_syntax -> proto_const_syntax
    4.14    val activate_const_syntax: theory -> literals
    4.15      -> proto_const_syntax -> Code_Thingol.naming -> const_syntax * Code_Thingol.naming
    4.16 -  val gen_print_app: (thm -> var_ctxt -> const * iterm list -> Pretty.T list)
    4.17 -    -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
    4.18 +  val gen_print_app: (thm option -> var_ctxt -> const * iterm list -> Pretty.T list)
    4.19 +    -> (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
    4.20      -> (string -> const_syntax option)
    4.21 -    -> thm -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
    4.22 -  val gen_print_bind: (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
    4.23 -    -> thm -> fixity
    4.24 +    -> thm option -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
    4.25 +  val gen_print_bind: (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
    4.26 +    -> thm option -> fixity
    4.27      -> iterm -> var_ctxt -> Pretty.T * var_ctxt
    4.28  
    4.29    val mk_name_module: Name.context -> string option -> (string -> string option)
    4.30 @@ -96,7 +96,8 @@
    4.31  
    4.32  open Code_Thingol;
    4.33  
    4.34 -fun eqn_error thm s = error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm);
    4.35 +fun eqn_error (SOME thm) s = error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm)
    4.36 +  | eqn_error NONE s = error s;
    4.37  
    4.38  (** assembling and printing text pieces **)
    4.39  
    4.40 @@ -243,9 +244,9 @@
    4.41    -> fixity -> (iterm * itype) list -> Pretty.T);
    4.42  type proto_const_syntax = int * (string list * (literals -> string list
    4.43    -> (var_ctxt -> fixity -> iterm -> Pretty.T)
    4.44 -    -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T));
    4.45 +    -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T));
    4.46  type const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
    4.47 -  -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
    4.48 +  -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
    4.49  
    4.50  fun simple_const_syntax syn =
    4.51    apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars)))) syn;
     5.1 --- a/src/Tools/Code/code_scala.ML	Fri Feb 19 11:06:22 2010 +0100
     5.2 +++ b/src/Tools/Code/code_scala.ML	Fri Feb 19 11:06:22 2010 +0100
     5.3 @@ -34,33 +34,33 @@
     5.4        Pretty.block [p, str ":", Pretty.brk 1, print_typ tyvars NOBR ty]
     5.5      fun print_var vars NONE = str "_"
     5.6        | print_var vars (SOME v) = (str o lookup_var vars) v
     5.7 -    fun print_term tyvars is_pat thm vars fxy (IConst c) =
     5.8 -          print_app tyvars is_pat thm vars fxy (c, [])
     5.9 -      | print_term tyvars is_pat thm vars fxy (t as (t1 `$ t2)) =
    5.10 +    fun print_term tyvars is_pat some_thm vars fxy (IConst c) =
    5.11 +          print_app tyvars is_pat some_thm vars fxy (c, [])
    5.12 +      | print_term tyvars is_pat some_thm vars fxy (t as (t1 `$ t2)) =
    5.13            (case Code_Thingol.unfold_const_app t
    5.14 -           of SOME app => print_app tyvars is_pat thm vars fxy app
    5.15 +           of SOME app => print_app tyvars is_pat some_thm vars fxy app
    5.16              | _ => applify "(" ")" fxy
    5.17 -                (print_term tyvars is_pat thm vars BR t1)
    5.18 -                [print_term tyvars is_pat thm vars NOBR t2])
    5.19 -      | print_term tyvars is_pat thm vars fxy (IVar v) =
    5.20 +                (print_term tyvars is_pat some_thm vars BR t1)
    5.21 +                [print_term tyvars is_pat some_thm vars NOBR t2])
    5.22 +      | print_term tyvars is_pat some_thm vars fxy (IVar v) =
    5.23            print_var vars v
    5.24 -      | print_term tyvars is_pat thm vars fxy ((v, ty) `|=> t) =
    5.25 +      | print_term tyvars is_pat some_thm vars fxy ((v, ty) `|=> t) =
    5.26            let
    5.27              val vars' = intro_vars (the_list v) vars;
    5.28            in
    5.29              concat [
    5.30                Pretty.block [str "(", print_typed tyvars (print_var vars' v) ty, str ")"],
    5.31                str "=>",
    5.32 -              print_term tyvars false thm vars' NOBR t
    5.33 +              print_term tyvars false some_thm vars' NOBR t
    5.34              ]
    5.35            end 
    5.36 -      | print_term tyvars is_pat thm vars fxy (ICase (cases as (_, t0))) =
    5.37 +      | print_term tyvars is_pat some_thm vars fxy (ICase (cases as (_, t0))) =
    5.38            (case Code_Thingol.unfold_const_app t0
    5.39             of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
    5.40 -                then print_case tyvars thm vars fxy cases
    5.41 -                else print_app tyvars is_pat thm vars fxy c_ts
    5.42 -            | NONE => print_case tyvars thm vars fxy cases)
    5.43 -    and print_app tyvars is_pat thm vars fxy (app as ((c, ((tys, _), tys_args)), ts)) =
    5.44 +                then print_case tyvars some_thm vars fxy cases
    5.45 +                else print_app tyvars is_pat some_thm vars fxy c_ts
    5.46 +            | NONE => print_case tyvars some_thm vars fxy cases)
    5.47 +    and print_app tyvars is_pat some_thm vars fxy (app as ((c, ((tys, _), tys_args)), ts)) =
    5.48        let
    5.49          val k = length ts;
    5.50          val l = case syntax_const c of NONE => args_num c | SOME (l, _) => l;
    5.51 @@ -69,47 +69,47 @@
    5.52          val (no_syntax, print') = case syntax_const c
    5.53           of NONE => (true, fn ts => applify "(" ")" fxy
    5.54                (applify "[" "]" NOBR ((str o deresolve) c) (map (print_typ tyvars NOBR) tys'))
    5.55 -                (map (print_term tyvars is_pat thm vars NOBR) ts))
    5.56 +                (map (print_term tyvars is_pat some_thm vars NOBR) ts))
    5.57            | SOME (_, print) => (false, fn ts =>
    5.58 -              print (print_term tyvars is_pat thm) thm vars fxy (ts ~~ take l tys_args));
    5.59 +              print (print_term tyvars is_pat some_thm) some_thm vars fxy (ts ~~ take l tys_args));
    5.60        in if k = l then print' ts
    5.61        else if k < l then
    5.62 -        print_term tyvars is_pat thm vars fxy (Code_Thingol.eta_expand l app)
    5.63 +        print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
    5.64        else let
    5.65          val (ts1, ts23) = chop l ts;
    5.66        in
    5.67          Pretty.block (print' ts1 :: map (fn t => Pretty.block
    5.68 -          [str ".apply(", print_term tyvars is_pat thm vars NOBR t, str ")"]) ts23)
    5.69 +          [str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, str ")"]) ts23)
    5.70        end end
    5.71 -    and print_bind tyvars thm fxy p = gen_print_bind (print_term tyvars true) thm fxy p
    5.72 -    and print_case tyvars thm vars fxy (cases as ((_, [_]), _)) =
    5.73 +    and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars true) some_thm fxy p
    5.74 +    and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
    5.75            let
    5.76              val (binds, body) = Code_Thingol.unfold_let (ICase cases);
    5.77              fun print_match ((pat, ty), t) vars =
    5.78                vars
    5.79 -              |> print_bind tyvars thm BR pat
    5.80 +              |> print_bind tyvars some_thm BR pat
    5.81                |>> (fn p => semicolon [Pretty.block [str "val", Pretty.brk 1, p,
    5.82                  str ":", Pretty.brk 1, print_typ tyvars NOBR ty],
    5.83 -                  str "=", print_term tyvars false thm vars NOBR t])
    5.84 +                  str "=", print_term tyvars false some_thm vars NOBR t])
    5.85              val (ps, vars') = fold_map print_match binds vars;
    5.86            in
    5.87              brackify_block fxy
    5.88                (str "{")
    5.89 -              (ps @| print_term tyvars false thm vars' NOBR body)
    5.90 +              (ps @| print_term tyvars false some_thm vars' NOBR body)
    5.91                (str "}")
    5.92            end
    5.93 -      | print_case tyvars thm vars fxy (((t, ty), clauses as _ :: _), _) =
    5.94 +      | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
    5.95            let
    5.96              fun print_select (pat, body) =
    5.97                let
    5.98 -                val (p, vars') = print_bind tyvars thm NOBR pat vars;
    5.99 -              in concat [str "case", p, str "=>", print_term tyvars false thm vars' NOBR body] end;
   5.100 +                val (p, vars') = print_bind tyvars some_thm NOBR pat vars;
   5.101 +              in concat [str "case", p, str "=>", print_term tyvars false some_thm vars' NOBR body] end;
   5.102            in brackify_block fxy
   5.103 -            (concat [print_term tyvars false thm vars NOBR t, str "match", str "{"])
   5.104 +            (concat [print_term tyvars false some_thm vars NOBR t, str "match", str "{"])
   5.105              (map print_select clauses)
   5.106              (str "}") 
   5.107            end
   5.108 -      | print_case tyvars thm vars fxy ((_, []), _) =
   5.109 +      | print_case tyvars some_thm vars fxy ((_, []), _) =
   5.110            (brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"];
   5.111      fun implicit_arguments tyvars vs vars =
   5.112        let
   5.113 @@ -140,7 +140,7 @@
   5.114                end
   5.115            | eqs =>
   5.116                let
   5.117 -                val tycos = fold (fn ((ts, t), (thm, _)) =>
   5.118 +                val tycos = fold (fn ((ts, t), _) =>
   5.119                    fold Code_Thingol.add_tyconames (t :: ts)) eqs [];
   5.120                  val tyvars = reserved
   5.121                    |> intro_base_names
   5.122 @@ -164,12 +164,12 @@
   5.123                    (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (tys2, ty1);
   5.124                  fun print_tuple [p] = p
   5.125                    | print_tuple ps = enum "," "(" ")" ps;
   5.126 -                fun print_rhs vars' ((_, t), (thm, _)) = print_term tyvars false thm vars' NOBR t;
   5.127 -                fun print_clause (eq as ((ts, _), (thm, _))) =
   5.128 +                fun print_rhs vars' ((_, t), (some_thm, _)) = print_term tyvars false some_thm vars' NOBR t;
   5.129 +                fun print_clause (eq as ((ts, _), (some_thm, _))) =
   5.130                    let
   5.131                      val vars' = intro_vars ((fold o Code_Thingol.fold_varnames) (insert (op =)) ts []) vars2;
   5.132                    in
   5.133 -                    concat [str "case", print_tuple (map (print_term tyvars true thm vars' NOBR) ts),
   5.134 +                    concat [str "case", print_tuple (map (print_term tyvars true some_thm vars' NOBR) ts),
   5.135                        str "=>", print_rhs vars' eq]
   5.136                    end;
   5.137                  val head = print_defhead tyvars vars3 ((str o deresolve) name) vs params tys1 implicit_ps ty2;
   5.138 @@ -267,7 +267,7 @@
   5.139                      auxs tys), str "=>"]];
   5.140                in 
   5.141                  concat ([str "val", (str o suffix "$" o deresolve_base) classparam,
   5.142 -                  str "="] @ args @ [print_app tyvars false thm vars NOBR (const, map (IVar o SOME) auxs)])
   5.143 +                  str "="] @ args @ [print_app tyvars false (SOME thm) vars NOBR (const, map (IVar o SOME) auxs)])
   5.144                end;
   5.145            in
   5.146              Pretty.chunks [
   5.147 @@ -352,15 +352,15 @@
   5.148       of Code_Thingol.Fun (_, ((_, ty), [])) => (length o fst o Code_Thingol.unfold_fun) ty
   5.149        | Code_Thingol.Fun (_, (_, ((ts, _), _) :: _)) => length ts
   5.150        | Code_Thingol.Datatypecons (_, tyco) =>
   5.151 -          let val Code_Thingol.Datatype (_, (_, dtcos)) = Graph.get_node program tyco
   5.152 -          in (length o the o AList.lookup (op =) dtcos) c end
   5.153 +          let val Code_Thingol.Datatype (_, (_, constrs)) = Graph.get_node program tyco
   5.154 +          in (length o the o AList.lookup (op =) constrs) c end
   5.155        | Code_Thingol.Classparam (_, class) =>
   5.156            let val Code_Thingol.Class (_, (_, (_, classparams))) = Graph.get_node program class
   5.157            in (length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =) classparams) c end;
   5.158      fun is_singleton c = case Graph.get_node program c
   5.159       of Code_Thingol.Datatypecons (_, tyco) =>
   5.160 -          let val Code_Thingol.Datatype (_, (_, dtcos)) = Graph.get_node program tyco
   5.161 -          in (null o the o AList.lookup (op =) dtcos) c end
   5.162 +          let val Code_Thingol.Datatype (_, (_, constrs)) = Graph.get_node program tyco
   5.163 +          in (null o the o AList.lookup (op =) constrs) c end
   5.164        | _ => false;
   5.165      val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
   5.166        reserved args_num is_singleton deresolver;