temporary adjustment to dubious state of eta expansion in recfun_codegen
authorhaftmann
Tue Aug 11 10:05:16 2009 +0200 (2009-08-11)
changeset 32356e11cd88e6ade
parent 32355 806d2df4d79d
child 32357 84a6d701e36f
temporary adjustment to dubious state of eta expansion in recfun_codegen
src/HOL/Lambda/WeakNorm.thy
src/HOL/MicroJava/J/JListExample.thy
src/HOL/MicroJava/J/State.thy
src/HOL/MicroJava/JVM/JVMListExample.thy
     1.1 --- a/src/HOL/Lambda/WeakNorm.thy	Mon Aug 10 13:34:50 2009 +0200
     1.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Tue Aug 11 10:05:16 2009 +0200
     1.3 @@ -444,7 +444,7 @@
     1.4    "default" ("(error \"default\")")
     1.5    "default :: 'a \<Rightarrow> 'b::default" ("(fn '_ => error \"default\")")
     1.6  
     1.7 -code_module Norm
     1.8 +(*code_module Norm
     1.9  contains
    1.10    test = "type_NF"
    1.11  
    1.12 @@ -509,6 +509,6 @@
    1.13  val ct2 = @{cterm "%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))"};
    1.14  val (dB2, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct2));
    1.15  val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2);
    1.16 -*}
    1.17 +*}*)
    1.18  
    1.19  end
     2.1 --- a/src/HOL/MicroJava/J/JListExample.thy	Mon Aug 10 13:34:50 2009 +0200
     2.2 +++ b/src/HOL/MicroJava/J/JListExample.thy	Tue Aug 11 10:05:16 2009 +0200
     2.3 @@ -1,12 +1,11 @@
     2.4  (*  Title:      HOL/MicroJava/J/JListExample.thy
     2.5 -    ID:         $Id$
     2.6      Author:     Stefan Berghofer
     2.7  *)
     2.8  
     2.9  header {* \isaheader{Example for generating executable code from Java semantics} *}
    2.10  
    2.11  theory JListExample
    2.12 -imports Eval SystemClasses
    2.13 +imports Eval
    2.14  begin
    2.15  
    2.16  ML {* Syntax.ambiguity_level := 100000 *}
     3.1 --- a/src/HOL/MicroJava/J/State.thy	Mon Aug 10 13:34:50 2009 +0200
     3.2 +++ b/src/HOL/MicroJava/J/State.thy	Tue Aug 11 10:05:16 2009 +0200
     3.3 @@ -1,12 +1,13 @@
     3.4  (*  Title:      HOL/MicroJava/J/State.thy
     3.5 -    ID:         $Id$
     3.6      Author:     David von Oheimb
     3.7      Copyright   1999 Technische Universitaet Muenchen
     3.8  *)
     3.9  
    3.10  header {* \isaheader{Program State} *}
    3.11  
    3.12 -theory State imports TypeRel Value begin
    3.13 +theory State
    3.14 +imports TypeRel Value
    3.15 +begin
    3.16  
    3.17  types 
    3.18    fields' = "(vname \<times> cname \<rightharpoonup> val)"  -- "field name, defining class, value"
    3.19 @@ -19,7 +20,10 @@
    3.20  
    3.21    init_vars :: "('a \<times> ty) list => ('a \<rightharpoonup> val)"
    3.22   "init_vars == map_of o map (\<lambda>(n,T). (n,default_val T))"
    3.23 -  
    3.24 +
    3.25 +lemma [code] (*manual eta expansion*):
    3.26 +  "init_vars xs = map_of (map (\<lambda>(n, T). (n, default_val T)) xs)"
    3.27 +  by (simp add: init_vars_def)
    3.28  
    3.29  types aheap  = "loc \<rightharpoonup> obj"    -- {* "@{text heap}" used in a translation below *}
    3.30        locals = "vname \<rightharpoonup> val"  -- "simple state, i.e. variable contents"
     4.1 --- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Mon Aug 10 13:34:50 2009 +0200
     4.2 +++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Tue Aug 11 10:05:16 2009 +0200
     4.3 @@ -1,11 +1,12 @@
     4.4  (*  Title:      HOL/MicroJava/JVM/JVMListExample.thy
     4.5 -    ID:         $Id$
     4.6      Author:     Stefan Berghofer
     4.7  *)
     4.8  
     4.9  header {* \isaheader{Example for generating executable code from JVM semantics}\label{sec:JVMListExample} *}
    4.10  
    4.11 -theory JVMListExample imports "../J/SystemClasses" JVMExec begin
    4.12 +theory JVMListExample
    4.13 +imports "../J/SystemClasses" JVMExec
    4.14 +begin
    4.15  
    4.16  consts
    4.17    list_nam :: cnam