non left-linear equations for nbe
authorhaftmann
Thu Sep 25 09:28:08 2008 +0200 (2008-09-25)
changeset 28350715163ec93c0
parent 28349 46a0dc9b51bb
child 28351 abfc66969d1f
non left-linear equations for nbe
NEWS
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/typecopy_package.ML
src/HOL/ex/NormalForm.thy
src/Pure/Isar/code.ML
src/Tools/code/code_funcgr.ML
src/Tools/code/code_haskell.ML
src/Tools/code/code_ml.ML
src/Tools/code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/NEWS	Thu Sep 25 09:28:07 2008 +0200
     1.2 +++ b/NEWS	Thu Sep 25 09:28:08 2008 +0200
     1.3 @@ -66,7 +66,10 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 -* HOL/Main: command "value" now integrates different evaluation
     1.8 +* Normalization by evaluation now allows non-leftlinear equations.
     1.9 +Declare with attribute [code nbe].
    1.10 +
    1.11 +* Command "value" now integrates different evaluation
    1.12  mechanisms.  The result of the first successful evaluation mechanism
    1.13  is printed.  In square brackets a particular named evaluation
    1.14  mechanisms may be specified (currently, [SML], [code] or [nbe]).  See
     2.1 --- a/src/HOL/Tools/datatype_codegen.ML	Thu Sep 25 09:28:07 2008 +0200
     2.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Thu Sep 25 09:28:08 2008 +0200
     2.3 @@ -433,9 +433,9 @@
     2.4    let
     2.5      val vs' = (map o apsnd)
     2.6        (curry (Sorts.inter_sort (Sign.classes_of thy)) [HOLogic.class_eq]) vs;
     2.7 -    fun add_def tyco lthy =
     2.8 +    fun add_def dtco lthy =
     2.9        let
    2.10 -        val ty = Type (tyco, map TFree vs');
    2.11 +        val ty = Type (dtco, map TFree vs');
    2.12          fun mk_side const_name = Const (const_name, ty --> ty --> HOLogic.boolT)
    2.13            $ Free ("x", ty) $ Free ("y", ty);
    2.14          val def = HOLogic.mk_Trueprop (HOLogic.mk_eq
    2.15 @@ -454,9 +454,15 @@
    2.16        |> map (MetaSimplifier.rewrite_rule [Thm.transfer thy @{thm equals_eq}]);
    2.17      fun add_eq_thms dtco thy =
    2.18        let
    2.19 +        val ty = Type (dtco, map TFree vs');
    2.20          val thy_ref = Theory.check_thy thy;
    2.21          val const = AxClass.param_of_inst thy (@{const_name eq_class.eq}, dtco);
    2.22 -        val get_thms = (fn () => get_eq' (Theory.deref thy_ref) dtco |> rev);
    2.23 +        val eq_refl = @{thm HOL.eq_refl}
    2.24 +          |> Thm.instantiate
    2.25 +              ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT ty)], [])
    2.26 +          |> Simpdata.mk_eq;
    2.27 +        fun get_thms () = (eq_refl, false)
    2.28 +          :: rev (map (rpair true) (get_eq' (Theory.deref thy_ref) dtco));
    2.29        in
    2.30          Code.add_funcl (const, Susp.delay get_thms) thy
    2.31        end;
     3.1 --- a/src/HOL/Tools/typecopy_package.ML	Thu Sep 25 09:28:07 2008 +0200
     3.2 +++ b/src/HOL/Tools/typecopy_package.ML	Thu Sep 25 09:28:08 2008 +0200
     3.3 @@ -124,10 +124,10 @@
     3.4    let
     3.5      val SOME { constr, proj_def, inject, vs, ... } = get_info thy tyco;
     3.6      val vs' = (map o apsnd) (curry (Sorts.inter_sort (Sign.classes_of thy)) [HOLogic.class_eq]) vs;
     3.7 -    val ty = Logic.unvarifyT (Sign.the_const_type thy constr);
     3.8 +    val ty = Type (tyco, map TFree vs');
     3.9 +    val ty_constr = Logic.unvarifyT (Sign.the_const_type thy constr);
    3.10      fun add_def tyco lthy =
    3.11        let
    3.12 -        val ty = Type (tyco, map TFree vs');
    3.13          fun mk_side const_name = Const (const_name, ty --> ty --> HOLogic.boolT)
    3.14            $ Free ("x", ty) $ Free ("y", ty);
    3.15          val def = HOLogic.mk_Trueprop (HOLogic.mk_eq
    3.16 @@ -140,16 +140,23 @@
    3.17        in (thm', lthy') end;
    3.18      fun tac thms = Class.intro_classes_tac []
    3.19        THEN ALLGOALS (ProofContext.fact_tac thms);
    3.20 -    fun add_eq_thm thy = 
    3.21 +    fun add_eq_thms thy = 
    3.22        let
    3.23          val eq = inject
    3.24            |> Code_Unit.constrain_thm [HOLogic.class_eq]
    3.25            |> Simpdata.mk_eq
    3.26            |> MetaSimplifier.rewrite_rule [Thm.transfer thy @{thm equals_eq}];
    3.27 -      in Code.add_func eq thy end;
    3.28 +        val eq_refl = @{thm HOL.eq_refl}
    3.29 +          |> Thm.instantiate
    3.30 +              ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT ty)], []);
    3.31 +      in
    3.32 +        thy
    3.33 +        |> Code.add_func eq
    3.34 +        |> Code.add_nonlinear_func eq_refl
    3.35 +      end;
    3.36    in
    3.37      thy
    3.38 -    |> Code.add_datatype [(constr, ty)]
    3.39 +    |> Code.add_datatype [(constr, ty_constr)]
    3.40      |> Code.add_func proj_def
    3.41      |> TheoryTarget.instantiation ([tyco], vs', [HOLogic.class_eq])
    3.42      |> add_def tyco
    3.43 @@ -157,7 +164,7 @@
    3.44      #> LocalTheory.exit
    3.45      #> ProofContext.theory_of
    3.46      #> Code.del_func thm
    3.47 -    #> add_eq_thm)
    3.48 +    #> add_eq_thms)
    3.49    end;
    3.50  
    3.51  val setup =
     4.1 --- a/src/HOL/ex/NormalForm.thy	Thu Sep 25 09:28:07 2008 +0200
     4.2 +++ b/src/HOL/ex/NormalForm.thy	Thu Sep 25 09:28:08 2008 +0200
     4.3 @@ -8,17 +8,30 @@
     4.4  imports Main "~~/src/HOL/Real/Rational"
     4.5  begin
     4.6  
     4.7 +lemma [code nbe]:
     4.8 +  "x = x \<longleftrightarrow> True" by rule+
     4.9 +
    4.10 +lemma [code nbe]:
    4.11 +  "eq_class.eq (x::bool) x \<longleftrightarrow> True" unfolding eq by rule+
    4.12 +
    4.13 +lemma [code nbe]:
    4.14 +  "eq_class.eq (x::nat) x \<longleftrightarrow> True" unfolding eq by rule+
    4.15 +
    4.16  lemma "True" by normalization
    4.17  lemma "p \<longrightarrow> True" by normalization
    4.18 -declare disj_assoc [code func]
    4.19 -lemma "((P | Q) | R) = (P | (Q | R))" by normalization rule
    4.20 +declare disj_assoc [code nbe]
    4.21 +lemma "((P | Q) | R) = (P | (Q | R))" by normalization
    4.22  declare disj_assoc [code func del]
    4.23 -lemma "0 + (n::nat) = n" by normalization rule
    4.24 -lemma "0 + Suc n = Suc n" by normalization rule
    4.25 -lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization rule
    4.26 +lemma "0 + (n::nat) = n" by normalization
    4.27 +lemma "0 + Suc n = Suc n" by normalization
    4.28 +lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization
    4.29  lemma "~((0::nat) < (0::nat))" by normalization
    4.30  
    4.31  datatype n = Z | S n
    4.32 +
    4.33 +lemma [code nbe]:
    4.34 +  "eq_class.eq (x::n) x \<longleftrightarrow> True" unfolding eq by rule+
    4.35 +
    4.36  consts
    4.37    add :: "n \<Rightarrow> n \<Rightarrow> n"
    4.38    add2 :: "n \<Rightarrow> n \<Rightarrow> n"
    4.39 @@ -40,9 +53,9 @@
    4.40  lemma [code]: "add2 n Z = n"
    4.41    by(induct n) auto
    4.42  
    4.43 -lemma "add2 (add2 n m) k = add2 n (add2 m k)" by normalization rule
    4.44 -lemma "add2 (add2 (S n) (S m)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization rule
    4.45 -lemma "add2 (add2 (S n) (add2 (S m) Z)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization rule
    4.46 +lemma "add2 (add2 n m) k = add2 n (add2 m k)" by normalization
    4.47 +lemma "add2 (add2 (S n) (S m)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization
    4.48 +lemma "add2 (add2 (S n) (add2 (S m) Z)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization
    4.49  
    4.50  primrec
    4.51    "mul Z = (%n. Z)"
    4.52 @@ -59,18 +72,22 @@
    4.53  lemma "exp (S(S Z)) (S(S(S(S Z)))) = exp (S(S(S(S Z)))) (S(S Z))" by normalization
    4.54  
    4.55  lemma "(let ((x,y),(u,v)) = ((Z,Z),(Z,Z)) in add (add x y) (add u v)) = Z" by normalization
    4.56 -lemma "split (%x y. x) (a, b) = a" by normalization rule
    4.57 +lemma "split (%x y. x) (a, b) = a" by normalization
    4.58  lemma "(%((x,y),(u,v)). add (add x y) (add u v)) ((Z,Z),(Z,Z)) = Z" by normalization
    4.59  
    4.60  lemma "case Z of Z \<Rightarrow> True | S x \<Rightarrow> False" by normalization
    4.61  
    4.62  lemma "[] @ [] = []" by normalization
    4.63 -lemma "map f [x,y,z::'x] = [f x, f y, f z]" by normalization rule+
    4.64 -lemma "[a, b, c] @ xs = a # b # c # xs" by normalization rule+
    4.65 -lemma "[] @ xs = xs" by normalization rule
    4.66 -lemma "map (%f. f True) [id, g, Not] = [True, g True, False]" by normalization rule+
    4.67 +lemma "map f [x,y,z::'x] = [f x, f y, f z]" by normalization
    4.68 +lemma "[a, b, c] @ xs = a # b # c # xs" by normalization
    4.69 +lemma "[] @ xs = xs" by normalization
    4.70 +lemma "map (%f. f True) [id, g, Not] = [True, g True, False]" by normalization
    4.71 +
    4.72 +lemma [code nbe]:
    4.73 +  "eq_class.eq (x :: 'a\<Colon>eq list) x \<longleftrightarrow> True" unfolding eq by rule+
    4.74 +
    4.75  lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs" by normalization rule+
    4.76 -lemma "rev [a, b, c] = [c, b, a]" by normalization rule+
    4.77 +lemma "rev [a, b, c] = [c, b, a]" by normalization
    4.78  normal_form "rev (a#b#cs) = rev cs @ [b, a]"
    4.79  normal_form "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
    4.80  normal_form "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))"
    4.81 @@ -79,21 +96,24 @@
    4.82    by normalization
    4.83  normal_form "case xs of [] \<Rightarrow> True | x#xs \<Rightarrow> False"
    4.84  normal_form "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) xs = P"
    4.85 -lemma "let x = y in [x, x] = [y, y]" by normalization rule+
    4.86 -lemma "Let y (%x. [x,x]) = [y, y]" by normalization rule+
    4.87 +lemma "let x = y in [x, x] = [y, y]" by normalization
    4.88 +lemma "Let y (%x. [x,x]) = [y, y]" by normalization
    4.89  normal_form "case n of Z \<Rightarrow> True | S x \<Rightarrow> False"
    4.90 -lemma "(%(x,y). add x y) (S z,S z) = S (add z (S z))" by normalization rule+
    4.91 +lemma "(%(x,y). add x y) (S z,S z) = S (add z (S z))" by normalization
    4.92  normal_form "filter (%x. x) ([True,False,x]@xs)"
    4.93  normal_form "filter Not ([True,False,x]@xs)"
    4.94  
    4.95 -lemma "[x,y,z] @ [a,b,c] = [x, y, z, a, b, c]" by normalization rule+
    4.96 -lemma "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f]) = [a, b, c, d, e, f]" by normalization rule+
    4.97 +lemma "[x,y,z] @ [a,b,c] = [x, y, z, a, b, c]" by normalization
    4.98 +lemma "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f]) = [a, b, c, d, e, f]" by normalization
    4.99  lemma "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()] = [False, True]" by normalization
   4.100  
   4.101 -lemma "last [a, b, c] = c" by normalization rule
   4.102 -lemma "last ([a, b, c] @ xs) = last (c # xs)" by normalization rule
   4.103 +lemma "last [a, b, c] = c" by normalization
   4.104 +lemma "last ([a, b, c] @ xs) = last (c # xs)" by normalization
   4.105  
   4.106 -lemma "(2::int) + 3 - 1 + (- k) * 2 = 4 + - k * 2" by normalization rule
   4.107 +lemma [code nbe]:
   4.108 +  "eq_class.eq (x :: int) x \<longleftrightarrow> True" unfolding eq by rule+
   4.109 +
   4.110 +lemma "(2::int) + 3 - 1 + (- k) * 2 = 4 + - k * 2" by normalization
   4.111  lemma "(-4::int) * 2 = -8" by normalization
   4.112  lemma "abs ((-4::int) + 2 * 1) = 2" by normalization
   4.113  lemma "(2::int) + 3 = 5" by normalization
   4.114 @@ -111,10 +131,10 @@
   4.115  lemma "(42::rat) / 1704 = 1 / 284 + 3 / 142" by normalization
   4.116  normal_form "Suc 0 \<in> set ms"
   4.117  
   4.118 -lemma "f = f" by normalization rule+
   4.119 -lemma "f x = f x" by normalization rule+
   4.120 -lemma "(f o g) x = f (g x)" by normalization rule+
   4.121 -lemma "(f o id) x = f x" by normalization rule+
   4.122 +lemma "f = f" by normalization
   4.123 +lemma "f x = f x" by normalization
   4.124 +lemma "(f o g) x = f (g x)" by normalization
   4.125 +lemma "(f o id) x = f x" by normalization
   4.126  normal_form "(\<lambda>x. x)"
   4.127  
   4.128  (* Church numerals: *)
     5.1 --- a/src/Pure/Isar/code.ML	Thu Sep 25 09:28:07 2008 +0200
     5.2 +++ b/src/Pure/Isar/code.ML	Thu Sep 25 09:28:08 2008 +0200
     5.3 @@ -9,12 +9,13 @@
     5.4  signature CODE =
     5.5  sig
     5.6    val add_func: thm -> theory -> theory
     5.7 +  val add_nonlinear_func: thm -> theory -> theory
     5.8    val add_liberal_func: thm -> theory -> theory
     5.9    val add_default_func: thm -> theory -> theory
    5.10    val add_default_func_attr: Attrib.src
    5.11    val del_func: thm -> theory -> theory
    5.12    val del_funcs: string -> theory -> theory
    5.13 -  val add_funcl: string * thm list Susp.T -> theory -> theory
    5.14 +  val add_funcl: string * (thm * bool) list Susp.T -> theory -> theory
    5.15    val map_pre: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory
    5.16    val map_post: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory
    5.17    val add_inline: thm -> theory -> theory
    5.18 @@ -34,7 +35,7 @@
    5.19  
    5.20    val coregular_algebra: theory -> Sorts.algebra
    5.21    val operational_algebra: theory -> (sort -> sort) * Sorts.algebra
    5.22 -  val these_funcs: theory -> string -> thm list
    5.23 +  val these_funcs: theory -> string -> (thm * bool) list
    5.24    val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
    5.25    val get_datatype_of_constr: theory -> string -> string option
    5.26    val get_case_data: theory -> string -> (int * string list) option
    5.27 @@ -115,41 +116,38 @@
    5.28  
    5.29  (** logical and syntactical specification of executable code **)
    5.30  
    5.31 -(* defining equations with default flag and lazy theorems *)
    5.32 +(* defining equations with linear flag, default flag and lazy theorems *)
    5.33  
    5.34  fun pretty_lthms ctxt r = case Susp.peek r
    5.35 - of SOME thms => map (ProofContext.pretty_thm ctxt) thms
    5.36 + of SOME thms => map (ProofContext.pretty_thm ctxt o fst) thms
    5.37    | NONE => [Pretty.str "[...]"];
    5.38  
    5.39  fun certificate thy f r =
    5.40    case Susp.peek r
    5.41 -   of SOME thms => (Susp.value o f thy) thms
    5.42 +   of SOME thms => (Susp.value o burrow_fst (f thy)) thms
    5.43      | NONE => let
    5.44          val thy_ref = Theory.check_thy thy;
    5.45 -      in Susp.delay (fn () => (f (Theory.deref thy_ref) o Susp.force) r) end;
    5.46 +      in Susp.delay (fn () => (burrow_fst (f (Theory.deref thy_ref)) o Susp.force) r) end;
    5.47  
    5.48 -fun add_drop_redundant verbose thm thms =
    5.49 +fun add_drop_redundant (thm, linear) thms =
    5.50    let
    5.51 -    fun warn thm' = (if verbose
    5.52 -      then warning ("Code generator: dropping redundant defining equation\n" ^ Display.string_of_thm thm')
    5.53 -      else (); true);
    5.54      val thy = Thm.theory_of_thm thm;
    5.55      val args_of = snd o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
    5.56      val args = args_of thm;
    5.57 -    fun matches [] _ = true
    5.58 -      | matches (Var _ :: xs) [] = matches xs []
    5.59 -      | matches (_ :: _) [] = false
    5.60 -      | matches (x :: xs) (y :: ys) = Pattern.matches thy (x, y) andalso matches xs ys;
    5.61 -    fun drop thm' = matches args (args_of thm') andalso warn thm';
    5.62 -  in thm :: filter_out drop thms end;
    5.63 +    fun matches_args args' = length args <= length args' andalso
    5.64 +      Pattern.matchess thy (args, curry Library.take (length args) args');
    5.65 +    fun drop (thm', _) = if matches_args (args_of thm') then 
    5.66 +      (warning ("Code generator: dropping redundant defining equation\n" ^ Display.string_of_thm thm'); true)
    5.67 +      else false;
    5.68 +  in (thm, linear) :: filter_out drop thms end;
    5.69  
    5.70 -fun add_thm _ thm (false, thms) = (false, Susp.value (add_drop_redundant true thm (Susp.force thms)))
    5.71 -  | add_thm true thm (true, thms) = (true, Susp.value (Susp.force thms @ [thm]))
    5.72 +fun add_thm _ thm (false, thms) = (false, Susp.map_force (add_drop_redundant thm) thms)
    5.73 +  | add_thm true thm (true, thms) = (true, Susp.map_force (fn thms => thms @ [thm]) thms)
    5.74    | add_thm false thm (true, thms) = (false, Susp.value [thm]);
    5.75  
    5.76  fun add_lthms lthms _ = (false, lthms);
    5.77  
    5.78 -fun del_thm thm = apsnd (Susp.value o remove Thm.eq_thm_prop thm o Susp.force);
    5.79 +fun del_thm thm = (apsnd o Susp.map_force) (remove (eq_fst Thm.eq_thm_prop) (thm, true));
    5.80  
    5.81  fun merge_defthms ((true, _), defthms2) = defthms2
    5.82    | merge_defthms (defthms1 as (false, _), (true, _)) = defthms1
    5.83 @@ -173,7 +171,7 @@
    5.84  (* specification data *)
    5.85  
    5.86  datatype spec = Spec of {
    5.87 -  funcs: (bool * thm list Susp.T) Symtab.table,
    5.88 +  funcs: (bool * (thm * bool) list Susp.T) Symtab.table,
    5.89    dtyps: ((string * sort) list * (string * typ list) list) Symtab.table,
    5.90    cases: (int * string list) Symtab.table * unit Symtab.table
    5.91  };
    5.92 @@ -479,7 +477,7 @@
    5.93      val funcs = classparams
    5.94        |> map_filter (fn c => try (AxClass.param_of_inst thy) (c, tyco))
    5.95        |> map (Symtab.lookup ((the_funcs o the_exec) thy))
    5.96 -      |> (map o Option.map) (Susp.force o snd)
    5.97 +      |> (map o Option.map) (map fst o Susp.force o snd)
    5.98        |> maps these
    5.99        |> map (Thm.transfer thy);
   5.100      fun sorts_of [Type (_, tys)] = map (snd o dest_TVar) tys
   5.101 @@ -600,9 +598,10 @@
   5.102          | NONE => check_typ_fun (c, thm);
   5.103    in check_typ (const_of_func thy thm, thm) end;
   5.104  
   5.105 -val mk_func = Code_Unit.error_thm (assert_func_typ o Code_Unit.mk_func);
   5.106 -val mk_liberal_func = Code_Unit.warning_thm (assert_func_typ o Code_Unit.mk_func);
   5.107 -val mk_default_func = Code_Unit.try_thm (assert_func_typ o Code_Unit.mk_func);
   5.108 +fun mk_func linear = Code_Unit.error_thm (assert_func_typ o Code_Unit.mk_func linear);
   5.109 +val mk_liberal_func = Code_Unit.warning_thm (assert_func_typ o Code_Unit.mk_func true);
   5.110 +val mk_syntactic_func = Code_Unit.warning_thm (assert_func_typ o Code_Unit.mk_func false);
   5.111 +val mk_default_func = Code_Unit.try_thm (assert_func_typ o Code_Unit.mk_func true);
   5.112  
   5.113  end; (*local*)
   5.114  
   5.115 @@ -641,8 +640,8 @@
   5.116  
   5.117  val is_undefined = Symtab.defined o snd o the_cases o the_exec;
   5.118  
   5.119 -fun gen_add_func strict default thm thy =
   5.120 -  case (if strict then SOME o mk_func else mk_liberal_func) thm
   5.121 +fun gen_add_func linear strict default thm thy =
   5.122 +  case (if strict then SOME o mk_func linear else mk_liberal_func) thm
   5.123     of SOME func =>
   5.124          let
   5.125            val c = const_of_func thy func;
   5.126 @@ -656,15 +655,16 @@
   5.127              else ();
   5.128          in
   5.129            (map_exec_purge (SOME [c]) o map_funcs) (Symtab.map_default
   5.130 -            (c, (true, Susp.value [])) (add_thm default func)) thy
   5.131 +            (c, (true, Susp.value [])) (add_thm default (func, linear))) thy
   5.132          end
   5.133      | NONE => thy;
   5.134  
   5.135 -val add_func = gen_add_func true false;
   5.136 -val add_liberal_func = gen_add_func false false;
   5.137 -val add_default_func = gen_add_func false true;
   5.138 +val add_func = gen_add_func true true false;
   5.139 +val add_liberal_func = gen_add_func true false false;
   5.140 +val add_default_func = gen_add_func true false true;
   5.141 +val add_nonlinear_func = gen_add_func false true false;
   5.142  
   5.143 -fun del_func thm thy = case mk_liberal_func thm
   5.144 +fun del_func thm thy = case mk_syntactic_func thm
   5.145   of SOME func => let
   5.146          val c = const_of_func thy func;
   5.147        in map_exec_purge (SOME [c]) (map_funcs
   5.148 @@ -762,6 +762,7 @@
   5.149    in
   5.150      TypeInterpretation.init
   5.151      #> add_del_attribute ("func", (add_func, del_func))
   5.152 +    #> add_simple_attribute ("nbe", add_nonlinear_func)
   5.153      #> add_del_attribute ("inline", (add_inline, del_inline))
   5.154      #> add_del_attribute ("post", (add_post, del_post))
   5.155    end));
   5.156 @@ -801,7 +802,7 @@
   5.157      thms
   5.158      |> apply_functrans thy
   5.159      |> map (Code_Unit.rewrite_func pre)
   5.160 -    (*FIXME - must check gere: rewrite rule, defining equation, proper constant *)
   5.161 +    (*FIXME - must check here: rewrite rule, defining equation, proper constant *)
   5.162      |> map (AxClass.unoverload thy)
   5.163      |> common_typ_funcs
   5.164    end;
   5.165 @@ -847,24 +848,24 @@
   5.166    Symtab.lookup ((the_funcs o the_exec) thy) const
   5.167    |> Option.map (Susp.force o snd)
   5.168    |> these
   5.169 -  |> map (Thm.transfer thy);
   5.170 +  |> (map o apfst) (Thm.transfer thy);
   5.171  
   5.172  in
   5.173  
   5.174  fun these_funcs thy const =
   5.175    let
   5.176      fun drop_refl thy = filter_out (is_equal o Term.fast_term_ord o Logic.dest_equals
   5.177 -      o ObjectLogic.drop_judgment thy o Thm.plain_prop_of);
   5.178 +      o ObjectLogic.drop_judgment thy o Thm.plain_prop_of o fst);
   5.179    in
   5.180      get_funcs thy const
   5.181 -    |> preprocess thy
   5.182 +    |> burrow_fst (preprocess thy)
   5.183      |> drop_refl thy
   5.184    end;
   5.185  
   5.186  fun default_typ thy c = case default_typ_proto thy c
   5.187   of SOME ty => Code_Unit.typscheme thy (c, ty)
   5.188    | NONE => (case get_funcs thy c
   5.189 -     of thm :: _ => snd (Code_Unit.head_func (AxClass.unoverload thy thm))
   5.190 +     of (thm, _) :: _ => snd (Code_Unit.head_func (AxClass.unoverload thy thm))
   5.191        | [] => Code_Unit.typscheme thy (c, Sign.the_const_type thy c));
   5.192  
   5.193  end; (*local*)
     6.1 --- a/src/Tools/code/code_funcgr.ML	Thu Sep 25 09:28:07 2008 +0200
     6.2 +++ b/src/Tools/code/code_funcgr.ML	Thu Sep 25 09:28:08 2008 +0200
     6.3 @@ -9,7 +9,7 @@
     6.4  signature CODE_FUNCGR =
     6.5  sig
     6.6    type T
     6.7 -  val funcs: T -> string -> thm list
     6.8 +  val funcs: T -> string -> (thm * bool) list
     6.9    val typ: T -> string -> (string * sort) list * typ
    6.10    val all: T -> string list
    6.11    val pretty: theory -> T -> Pretty.T
    6.12 @@ -24,7 +24,7 @@
    6.13  
    6.14  (** the graph type **)
    6.15  
    6.16 -type T = (((string * sort) list * typ) * thm list) Graph.T;
    6.17 +type T = (((string * sort) list * typ) * (thm * bool) list) Graph.T;
    6.18  
    6.19  fun funcs funcgr =
    6.20    these o Option.map snd o try (Graph.get_node funcgr);
    6.21 @@ -41,7 +41,7 @@
    6.22    |> map (fn (s, thms) =>
    6.23         (Pretty.block o Pretty.fbreaks) (
    6.24           Pretty.str s
    6.25 -         :: map Display.pretty_thm thms
    6.26 +         :: map (Display.pretty_thm o fst) thms
    6.27         ))
    6.28    |> Pretty.chunks;
    6.29  
    6.30 @@ -57,7 +57,7 @@
    6.31    | consts_of (const, thms as _ :: _) = 
    6.32        let
    6.33          fun the_const (c, _) = if c = const then I else insert (op =) c
    6.34 -      in fold_consts the_const thms [] end;
    6.35 +      in fold_consts the_const (map fst thms) [] end;
    6.36  
    6.37  fun insts_of thy algebra tys sorts =
    6.38    let
    6.39 @@ -100,19 +100,19 @@
    6.40  fun resort_funcss thy algebra funcgr =
    6.41    let
    6.42      val typ_funcgr = try (fst o Graph.get_node funcgr);
    6.43 -    val resort_dep = apsnd (resort_thms thy algebra typ_funcgr);
    6.44 +    val resort_dep = (apsnd o burrow_fst) (resort_thms thy algebra typ_funcgr);
    6.45      fun resort_rec typ_of (c, []) = (true, (c, []))
    6.46 -      | resort_rec typ_of (c, thms as thm :: _) = if is_some (AxClass.inst_of_param thy c)
    6.47 +      | resort_rec typ_of (c, thms as (thm, _) :: _) = if is_some (AxClass.inst_of_param thy c)
    6.48            then (true, (c, thms))
    6.49            else let
    6.50              val (_, (vs, ty)) = Code_Unit.head_func thm;
    6.51 -            val thms' as thm' :: _ = resort_thms thy algebra typ_of thms
    6.52 +            val thms' as (thm', _) :: _ = burrow_fst (resort_thms thy algebra typ_of) thms
    6.53              val (_, (vs', ty')) = Code_Unit.head_func thm'; (*FIXME simplify check*)
    6.54            in (Sign.typ_equiv thy (ty, ty'), (c, thms')) end;
    6.55      fun resort_recs funcss =
    6.56        let
    6.57          fun typ_of c = case these (AList.lookup (op =) funcss c)
    6.58 -         of thm :: _ => (SOME o snd o Code_Unit.head_func) thm
    6.59 +         of (thm, _) :: _ => (SOME o snd o Code_Unit.head_func) thm
    6.60            | [] => NONE;
    6.61          val (unchangeds, funcss') = split_list (map (resort_rec typ_of) funcss);
    6.62          val unchanged = fold (fn x => fn y => x andalso y) unchangeds true;
    6.63 @@ -158,8 +158,8 @@
    6.64      |> pair (SOME const)
    6.65    else let
    6.66      val thms = Code.these_funcs thy const
    6.67 -      |> Code_Unit.norm_args
    6.68 -      |> Code_Unit.norm_varnames Code_Name.purify_tvar Code_Name.purify_var;
    6.69 +      |> burrow_fst Code_Unit.norm_args
    6.70 +      |> burrow_fst (Code_Unit.norm_varnames Code_Name.purify_tvar Code_Name.purify_var);
    6.71      val rhs = consts_of (const, thms);
    6.72    in
    6.73      auxgr
    6.74 @@ -182,14 +182,14 @@
    6.75        |> resort_funcss thy algebra funcgr
    6.76        |> filter_out (can (Graph.get_node funcgr) o fst);
    6.77      fun typ_func c [] = Code.default_typ thy c
    6.78 -      | typ_func c (thms as thm :: _) = (snd o Code_Unit.head_func) thm;
    6.79 +      | typ_func c (thms as (thm, _) :: _) = (snd o Code_Unit.head_func) thm;
    6.80      fun add_funcs (const, thms) =
    6.81        Graph.new_node (const, (typ_func const thms, thms));
    6.82      fun add_deps (funcs as (const, thms)) funcgr =
    6.83        let
    6.84          val deps = consts_of funcs;
    6.85          val insts = instances_of_consts thy algebra funcgr
    6.86 -          (fold_consts (insert (op =)) thms []);
    6.87 +          (fold_consts (insert (op =)) (map fst thms) []);
    6.88        in
    6.89          funcgr
    6.90          |> ensure_consts thy algebra insts
    6.91 @@ -278,16 +278,15 @@
    6.92  
    6.93  (** diagnostic commands **)
    6.94  
    6.95 -fun code_depgr thy [] = make thy []
    6.96 -  | code_depgr thy consts =
    6.97 -      let
    6.98 -        val gr = make thy consts;
    6.99 -        val select = Graph.all_succs gr consts;
   6.100 -      in
   6.101 -        gr
   6.102 -        |> Graph.subgraph (member (op =) select) 
   6.103 -        |> Graph.map_nodes ((apsnd o map) (AxClass.overload thy))
   6.104 -      end;
   6.105 +fun code_depgr thy consts =
   6.106 +  let
   6.107 +    val gr = make thy consts;
   6.108 +    val select = Graph.all_succs gr consts;
   6.109 +  in
   6.110 +    gr
   6.111 +    |> not (null consts) ? Graph.subgraph (member (op =) select) 
   6.112 +    |> Graph.map_nodes ((apsnd o map o apfst) (AxClass.overload thy))
   6.113 +  end;
   6.114  
   6.115  fun code_thms thy = Pretty.writeln o pretty thy o code_depgr thy;
   6.116  
     7.1 --- a/src/Tools/code/code_haskell.ML	Thu Sep 25 09:28:07 2008 +0200
     7.2 +++ b/src/Tools/code/code_haskell.ML	Thu Sep 25 09:28:08 2008 +0200
     7.3 @@ -153,10 +153,11 @@
     7.4                )
     7.5              ]
     7.6            end
     7.7 -      | pr_stmt (name, Code_Thingol.Fun ((vs, ty), eqs)) =
     7.8 +      | pr_stmt (name, Code_Thingol.Fun ((vs, ty), raw_eqs)) =
     7.9            let
    7.10 +            val eqs = filter (snd o snd) raw_eqs;
    7.11              val tyvars = intro_vars (map fst vs) init_syms;
    7.12 -            fun pr_eq ((ts, t), thm) =
    7.13 +            fun pr_eq ((ts, t), (thm, _)) =
    7.14                let
    7.15                  val consts = map_filter
    7.16                    (fn c => if (is_some o syntax_const) c
    7.17 @@ -248,7 +249,7 @@
    7.18        | pr_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
    7.19            let
    7.20              val tyvars = intro_vars (map fst vs) init_syms;
    7.21 -            fun pr_instdef ((classparam, c_inst), thm) =
    7.22 +            fun pr_instdef ((classparam, c_inst), (thm, _)) =
    7.23                semicolon [
    7.24                  (str o classparam_name class) classparam,
    7.25                  str "=",
     8.1 --- a/src/Tools/code/code_ml.ML	Thu Sep 25 09:28:07 2008 +0200
     8.2 +++ b/src/Tools/code/code_ml.ML	Thu Sep 25 09:28:08 2008 +0200
     8.3 @@ -27,12 +27,12 @@
     8.4  val target_OCaml = "OCaml";
     8.5  
     8.6  datatype ml_stmt =
     8.7 -    MLFuns of (string * (typscheme * ((iterm list * iterm) * thm) list)) list
     8.8 +    MLFuns of (string * (typscheme * ((iterm list * iterm) * (thm * bool)) list)) list
     8.9    | MLDatas of (string * ((vname * sort) list * (string * itype list) list)) list
    8.10    | MLClass of string * (vname * ((class * string) list * (string * itype) list))
    8.11    | MLClassinst of string * ((class * (string * (vname * sort) list))
    8.12          * ((class * (string * (string * dict list list))) list
    8.13 -      * ((string * const) * thm) list));
    8.14 +      * ((string * const) * (thm * bool)) list));
    8.15  
    8.16  fun stmt_names_of (MLFuns fs) = map fst fs
    8.17    | stmt_names_of (MLDatas ds) = map fst ds
    8.18 @@ -192,7 +192,7 @@
    8.19                      val vs_dict = filter_out (null o snd) vs;
    8.20                      val shift = if null eqs' then I else
    8.21                        map (Pretty.block o single o Pretty.block o single);
    8.22 -                    fun pr_eq definer ((ts, t), thm) =
    8.23 +                    fun pr_eq definer ((ts, t), (thm, _)) =
    8.24                        let
    8.25                          val consts = map_filter
    8.26                            (fn c => if (is_some o syntax_const) c
    8.27 @@ -299,7 +299,7 @@
    8.28                  str "=",
    8.29                  pr_dicts NOBR [DictConst dss]
    8.30                ];
    8.31 -            fun pr_classparam ((classparam, c_inst), thm) =
    8.32 +            fun pr_classparam ((classparam, c_inst), (thm, _)) =
    8.33                concat [
    8.34                  (str o pr_label_classparam) classparam,
    8.35                  str "=",
    8.36 @@ -453,7 +453,7 @@
    8.37        in map (lookup_var vars') fished3 end;
    8.38      fun pr_stmt (MLFuns (funns as funn :: funns')) =
    8.39            let
    8.40 -            fun pr_eq ((ts, t), thm) =
    8.41 +            fun pr_eq ((ts, t), (thm, _)) =
    8.42                let
    8.43                  val consts = map_filter
    8.44                    (fn c => if (is_some o syntax_const) c
    8.45 @@ -481,7 +481,7 @@
    8.46                        @@ str exc_str
    8.47                      )
    8.48                    end
    8.49 -              | pr_eqs _ _ [((ts, t), thm)] =
    8.50 +              | pr_eqs _ _ [((ts, t), (thm, _))] =
    8.51                    let
    8.52                      val consts = map_filter
    8.53                        (fn c => if (is_some o syntax_const) c
    8.54 @@ -611,7 +611,7 @@
    8.55                  str "=",
    8.56                  pr_dicts NOBR [DictConst dss]
    8.57                ];
    8.58 -            fun pr_classparam_inst ((classparam, c_inst), thm) =
    8.59 +            fun pr_classparam_inst ((classparam, c_inst), (thm, _)) =
    8.60                concat [
    8.61                  (str o deresolve) classparam,
    8.62                  str "=",
    8.63 @@ -727,7 +727,7 @@
    8.64        fold_map
    8.65          (fn (name, Code_Thingol.Fun stmt) =>
    8.66                map_nsp_fun_yield (mk_name_stmt false name) #>>
    8.67 -                rpair (name, stmt)
    8.68 +                rpair (name, stmt |> apsnd (filter (snd o snd)))
    8.69            | (name, _) =>
    8.70                error ("Function block containing illegal statement: " ^ labelled_name name)
    8.71          ) stmts
    8.72 @@ -895,7 +895,8 @@
    8.73          val _ = if Code_Thingol.contains_dictvar t then
    8.74            error "Term to be evaluated constains free dictionaries" else ();
    8.75          val program' = program
    8.76 -          |> Graph.new_node (Code_Name.value_name, Code_Thingol.Fun (([], ty), [(([], t), Drule.dummy_thm)]))
    8.77 +          |> Graph.new_node (Code_Name.value_name,
    8.78 +              Code_Thingol.Fun (([], ty), [(([], t), (Drule.dummy_thm, true))]))
    8.79            |> fold (curry Graph.add_edge Code_Name.value_name) deps;
    8.80          val (value_code, [value_name']) = ml_code_of thy program' [Code_Name.value_name];
    8.81          val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
     9.1 --- a/src/Tools/code/code_thingol.ML	Thu Sep 25 09:28:07 2008 +0200
     9.2 +++ b/src/Tools/code/code_thingol.ML	Thu Sep 25 09:28:08 2008 +0200
     9.3 @@ -62,7 +62,7 @@
     9.4  
     9.5    datatype stmt =
     9.6        NoStmt
     9.7 -    | Fun of typscheme * ((iterm list * iterm) * thm) list
     9.8 +    | Fun of typscheme * ((iterm list * iterm) * (thm * bool)) list
     9.9      | Datatype of (vname * sort) list * (string * itype list) list
    9.10      | Datatypecons of string
    9.11      | Class of vname * ((class * string) list * (string * itype) list)
    9.12 @@ -70,7 +70,7 @@
    9.13      | Classparam of class
    9.14      | Classinst of (class * (string * (vname * sort) list))
    9.15            * ((class * (string * (string * dict list list))) list
    9.16 -        * ((string * const) * thm) list);
    9.17 +        * ((string * const) * (thm * bool)) list);
    9.18    type program = stmt Graph.T;
    9.19    val empty_funs: program -> string list;
    9.20    val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm;
    9.21 @@ -258,7 +258,7 @@
    9.22  type typscheme = (vname * sort) list * itype;
    9.23  datatype stmt =
    9.24      NoStmt
    9.25 -  | Fun of typscheme * ((iterm list * iterm) * thm) list
    9.26 +  | Fun of typscheme * ((iterm list * iterm) * (thm * bool)) list
    9.27    | Datatype of (vname * sort) list * (string * itype list) list
    9.28    | Datatypecons of string
    9.29    | Class of vname * ((class * string) list * (string * itype) list)
    9.30 @@ -266,7 +266,7 @@
    9.31    | Classparam of class
    9.32    | Classinst of (class * (string * (vname * sort) list))
    9.33          * ((class * (string * (string * dict list list))) list
    9.34 -      * ((string * const) * thm) list);
    9.35 +      * ((string * const) * (thm * bool)) list);
    9.36  
    9.37  type program = stmt Graph.T;
    9.38  
    9.39 @@ -423,14 +423,14 @@
    9.40            fold_map (ensure_classrel thy algbr funcgr) classrels
    9.41            #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort))))
    9.42    in fold_map mk_dict typargs end
    9.43 -and exprgen_eq thy algbr funcgr thm =
    9.44 +and exprgen_eq thy algbr funcgr (thm, linear) =
    9.45    let
    9.46      val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
    9.47        o Logic.unvarify o prop_of) thm;
    9.48    in
    9.49      fold_map (exprgen_term thy algbr funcgr (SOME thm)) args
    9.50      ##>> exprgen_term thy algbr funcgr (SOME thm) rhs
    9.51 -    #>> rpair thm
    9.52 +    #>> rpair (thm, linear)
    9.53    end
    9.54  and ensure_inst thy (algbr as (_, algebra)) funcgr (class, tyco) =
    9.55    let
    9.56 @@ -457,7 +457,7 @@
    9.57        in
    9.58          ensure_const thy algbr funcgr c
    9.59          ##>> exprgen_const thy algbr funcgr (SOME thm) c_ty
    9.60 -        #>> (fn (c, IConst c_inst) => ((c, c_inst), thm))
    9.61 +        #>> (fn (c, IConst c_inst) => ((c, c_inst), (thm, true)))
    9.62        end;
    9.63      val stmt_inst =
    9.64        ensure_class thy algbr funcgr class
    9.65 @@ -485,7 +485,7 @@
    9.66          val ty = Logic.unvarifyT raw_ty;
    9.67          val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
    9.68            then raw_thms
    9.69 -          else map (Code_Unit.expand_eta 1) raw_thms;
    9.70 +          else (map o apfst) (Code_Unit.expand_eta 1) raw_thms;
    9.71        in
    9.72          trns
    9.73          |> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
    9.74 @@ -642,7 +642,7 @@
    9.75        fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
    9.76        ##>> exprgen_typ thy algbr funcgr ty
    9.77        ##>> exprgen_term thy algbr funcgr NONE t
    9.78 -      #>> (fn ((vs, ty), t) => Fun ((vs, ty), [(([], t), Drule.dummy_thm)]));
    9.79 +      #>> (fn ((vs, ty), t) => Fun ((vs, ty), [(([], t), (Drule.dummy_thm, true))]));
    9.80      fun term_value (dep, program1) =
    9.81        let
    9.82          val Fun ((vs, ty), [(([], t), _)]) =
    10.1 --- a/src/Tools/nbe.ML	Thu Sep 25 09:28:07 2008 +0200
    10.2 +++ b/src/Tools/nbe.ML	Thu Sep 25 09:28:08 2008 +0200
    10.3 @@ -15,10 +15,11 @@
    10.4      | Free of string * Univ list             (*free (uninterpreted) variables*)
    10.5      | DFree of string * int                  (*free (uninterpreted) dictionary parameters*)
    10.6      | BVar of int * Univ list
    10.7 -    | Abs of (int * (Univ list -> Univ)) * Univ list;
    10.8 +    | Abs of (int * (Univ list -> Univ)) * Univ list
    10.9    val apps: Univ -> Univ list -> Univ        (*explicit applications*)
   10.10    val abss: int -> (Univ list -> Univ) -> Univ
   10.11                                               (*abstractions as closures*)
   10.12 +  val same: Univ -> Univ -> bool
   10.13  
   10.14    val univs_ref: (unit -> Univ list -> Univ list) option ref
   10.15    val trace: bool ref
   10.16 @@ -63,6 +64,13 @@
   10.17    | Abs of (int * (Univ list -> Univ)) * Univ list
   10.18                                         (*abstractions as closures*);
   10.19  
   10.20 +fun same (Const (k, xs)) (Const (l, ys)) = k = l andalso sames xs ys
   10.21 +  | same (Free (s, xs)) (Free (t, ys)) = s = t andalso sames xs ys
   10.22 +  | same (DFree (s, k)) (DFree (t, l)) = s = t andalso k = l
   10.23 +  | same (BVar (k, xs)) (BVar (l, ys)) = k = l andalso sames xs ys
   10.24 +  | same _ _ = false
   10.25 +and sames xs ys = length xs = length ys andalso forall (uncurry same) (xs ~~ ys);
   10.26 +
   10.27  (* constructor functions *)
   10.28  
   10.29  fun abss n f = Abs ((n, f), []);
   10.30 @@ -92,6 +100,11 @@
   10.31  fun ml_Let d e = "let\n" ^ d ^ " in " ^ e ^ " end";
   10.32  fun ml_as v t = "(" ^ v ^ " as " ^ t ^ ")";
   10.33  
   10.34 +fun ml_and [] = "true"
   10.35 +  | ml_and [x] = x
   10.36 +  | ml_and xs = "(" ^ space_implode " andalso " xs ^ ")";
   10.37 +fun ml_if b x y = "(if " ^ b ^ " then " ^ x ^ " else " ^ y ^ ")";
   10.38 +
   10.39  fun ml_list es = "[" ^ commas es ^ "]";
   10.40  
   10.41  fun ml_fundefs ([(name, [([], e)])]) =
   10.42 @@ -113,11 +126,12 @@
   10.43  val univs_ref = ref (NONE : (unit -> Univ list -> Univ list) option);
   10.44  
   10.45  local
   10.46 -  val prefix =          "Nbe.";
   10.47 -  val name_ref =        prefix ^ "univs_ref";
   10.48 -  val name_const =      prefix ^ "Const";
   10.49 -  val name_abss =       prefix ^ "abss";
   10.50 -  val name_apps =       prefix ^ "apps";
   10.51 +  val prefix =      "Nbe.";
   10.52 +  val name_ref =    prefix ^ "univs_ref";
   10.53 +  val name_const =  prefix ^ "Const";
   10.54 +  val name_abss =   prefix ^ "abss";
   10.55 +  val name_apps =   prefix ^ "apps";
   10.56 +  val name_same =   prefix ^ "same";
   10.57  in
   10.58  
   10.59  val univs_cookie = (name_ref, univs_ref);
   10.60 @@ -141,6 +155,8 @@
   10.61  fun nbe_abss 0 f = f `$` ml_list []
   10.62    | nbe_abss n f = name_abss `$$` [string_of_int n, f];
   10.63  
   10.64 +fun nbe_same v1 v2 = "(" ^ name_same ^ " " ^ nbe_bound v1 ^ " " ^ nbe_bound v2 ^ ")";
   10.65 +
   10.66  end;
   10.67  
   10.68  open Basic_Code_Thingol;
   10.69 @@ -173,34 +189,62 @@
   10.70        | assemble_idict (DictVar (supers, (v, (n, _)))) =
   10.71            fold_rev (fn super => assemble_constapp super [] o single) supers (nbe_dict v n);
   10.72  
   10.73 -    fun assemble_iterm match_cont constapp =
   10.74 +    fun assemble_iterm constapp =
   10.75        let
   10.76 -        fun of_iterm t =
   10.77 +        fun of_iterm match_cont t =
   10.78            let
   10.79              val (t', ts) = Code_Thingol.unfold_app t
   10.80 -          in of_iapp t' (fold_rev (cons o of_iterm) ts []) end
   10.81 -        and of_iapp (IConst (c, (dss, _))) ts = constapp c dss ts
   10.82 -          | of_iapp (IVar v) ts = nbe_apps (nbe_bound v) ts
   10.83 -          | of_iapp ((v, _) `|-> t) ts =
   10.84 -              nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound v]) (of_iterm t))) ts
   10.85 -          | of_iapp (ICase (((t, _), cs), t0)) ts =
   10.86 -              nbe_apps (ml_cases (of_iterm t) (map (pairself of_iterm) cs
   10.87 -                @ [("_", case match_cont of SOME s => s | NONE => of_iterm t0)])) ts
   10.88 +          in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end
   10.89 +        and of_iapp match_cont (IConst (c, (dss, _))) ts = constapp c dss ts
   10.90 +          | of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound v) ts
   10.91 +          | of_iapp match_cont ((v, _) `|-> t) ts =
   10.92 +              nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound v]) (of_iterm NONE t))) ts
   10.93 +          | of_iapp match_cont (ICase (((t, _), cs), t0)) ts =
   10.94 +              nbe_apps (ml_cases (of_iterm NONE t)
   10.95 +                (map (fn (p, t) => (of_iterm NONE p, of_iterm match_cont t)) cs
   10.96 +                  @ [("_", case match_cont of SOME s => s | NONE => of_iterm NONE t0)])) ts
   10.97        in of_iterm end;
   10.98  
   10.99 +    fun subst_nonlin_vars args =
  10.100 +      let
  10.101 +        val vs = (fold o Code_Thingol.fold_varnames)
  10.102 +          (fn v => AList.map_default (op =) (v, 0) (curry (op +) 1)) args [];
  10.103 +        val names = Name.make_context (map fst vs);
  10.104 +        fun declare v k ctxt = let val vs = Name.invents ctxt v k
  10.105 +          in (vs, fold Name.declare vs ctxt) end;
  10.106 +        val (vs_renames, _) = fold_map (fn (v, k) => if k > 1
  10.107 +          then declare v (k - 1) #>> (fn vs => (v, vs))
  10.108 +          else pair (v, [])) vs names;
  10.109 +        val samepairs = maps (fn (v, vs) => map (pair v) vs) vs_renames;
  10.110 +        fun subst_vars (t as IConst _) samepairs = (t, samepairs)
  10.111 +          | subst_vars (t as IVar v) samepairs = (case AList.lookup (op =) samepairs v
  10.112 +             of SOME v' => (IVar v', AList.delete (op =) v samepairs)
  10.113 +              | NONE => (t, samepairs))
  10.114 +          | subst_vars (t1 `$ t2) samepairs = samepairs
  10.115 +              |> subst_vars t1
  10.116 +              ||>> subst_vars t2
  10.117 +              |>> (op `$)
  10.118 +          | subst_vars (ICase (_, t)) samepairs = subst_vars t samepairs;
  10.119 +        val (args', _) = fold_map subst_vars args samepairs;
  10.120 +      in (samepairs, args') end;
  10.121 +
  10.122      fun assemble_eqn c dicts default_args (i, (args, rhs)) =
  10.123        let
  10.124          val is_eval = (c = "");
  10.125          val default_rhs = nbe_apps_local (i+1) c (dicts @ default_args);
  10.126          val match_cont = if is_eval then NONE else SOME default_rhs;
  10.127 -        val assemble_arg = assemble_iterm NONE
  10.128 -          (fn c => fn _ => fn ts => nbe_apps_constr idx_of c ts);
  10.129 -        val assemble_rhs = assemble_iterm match_cont assemble_constapp;
  10.130 +        val assemble_arg = assemble_iterm
  10.131 +          (fn c => fn _ => fn ts => nbe_apps_constr idx_of c ts) NONE;
  10.132 +        val assemble_rhs = assemble_iterm assemble_constapp match_cont ;
  10.133 +        val (samepairs, args') = subst_nonlin_vars args;
  10.134 +        val s_args = map assemble_arg args';
  10.135 +        val s_rhs = if null samepairs then assemble_rhs rhs
  10.136 +          else ml_if (ml_and (map (uncurry nbe_same) samepairs))
  10.137 +            (assemble_rhs rhs) default_rhs;
  10.138          val eqns = if is_eval then
  10.139 -            [([ml_list (rev (dicts @ map assemble_arg args))], assemble_rhs rhs)]
  10.140 +            [([ml_list (rev (dicts @ s_args))], s_rhs)]
  10.141            else
  10.142 -            [([ml_list (rev (dicts @ map2 ml_as default_args
  10.143 -                (map assemble_arg args)))], assemble_rhs rhs),
  10.144 +            [([ml_list (rev (dicts @ map2 ml_as default_args s_args))], s_rhs),
  10.145                ([ml_list (rev (dicts @ default_args))], default_rhs)]
  10.146        in (nbe_fun i c, eqns) end;
  10.147