fixing code generation test
authorbulwahn
Thu Jun 09 09:07:13 2011 +0200 (2011-06-09)
changeset 43317f9283eb3a4bf
parent 43316 3e274608f06b
child 43318 825f4f0dcf71
fixing code generation test
src/HOL/Codegenerator_Test/Generate_Pretty.thy
src/HOL/Quickcheck_Narrowing.thy
src/HOL/Tools/Quickcheck/narrowing_generators.ML
     1.1 --- a/src/HOL/Codegenerator_Test/Generate_Pretty.thy	Thu Jun 09 08:32:22 2011 +0200
     1.2 +++ b/src/HOL/Codegenerator_Test/Generate_Pretty.thy	Thu Jun 09 09:07:13 2011 +0200
     1.3 @@ -10,6 +10,10 @@
     1.4  lemma [code, code del]: "nat_of_char = nat_of_char" ..
     1.5  lemma [code, code del]: "char_of_nat = char_of_nat" ..
     1.6  
     1.7 +declare Quickcheck_Narrowing.zero_code_int_code[code del]
     1.8 +declare Quickcheck_Narrowing.one_code_int_code[code del]
     1.9 +declare Quickcheck_Narrowing.int_of_code[code del]
    1.10 +
    1.11  subsection {* Check whether generated code compiles *}
    1.12  
    1.13  text {*
     2.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Thu Jun 09 08:32:22 2011 +0200
     2.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Thu Jun 09 09:07:13 2011 +0200
     2.3 @@ -207,6 +207,13 @@
     2.4  subsubsection {* Narrowing's deep representation of types and terms *}
     2.5  
     2.6  datatype narrowing_type = SumOfProd "narrowing_type list list"
     2.7 +text {*
     2.8 +The definition of the automatically derived equal type class instance for @{typ narrowing_type}
     2.9 +causes an error in the OCaml serializer.
    2.10 +For the moment, we delete this equation manually because we do not require an executable equality
    2.11 +on this type anyway.   
    2.12 +*}
    2.13 +declare Quickcheck_Narrowing.equal_narrowing_type_def[code del]
    2.14  
    2.15  datatype narrowing_term = Var "code_int list" narrowing_type | Ctr code_int "narrowing_term list"
    2.16  datatype 'a cons = C narrowing_type "(narrowing_term list => 'a) list"
     3.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Jun 09 08:32:22 2011 +0200
     3.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Jun 09 09:07:13 2011 +0200
     3.3 @@ -358,8 +358,8 @@
     3.4    end
     3.5  
     3.6  fun mk_case_term ctxt p ((@{const_name Ex}, (x, T)) :: qs') (Existential_Counterexample cs) =
     3.7 -    fst (Datatype.make_case ctxt Datatype_Case.Quiet [] (Free (x, T)) (map (fn (t, c) =>
     3.8 -      (t, mk_case_term ctxt (p - 1) qs' c)) cs))
     3.9 +    Datatype.make_case ctxt Datatype_Case.Quiet [] (Free (x, T)) (map (fn (t, c) =>
    3.10 +      (t, mk_case_term ctxt (p - 1) qs' c)) cs)
    3.11    | mk_case_term ctxt p ((@{const_name All}, (x, T)) :: qs') (Universal_Counterexample (t, c)) =
    3.12      if p = 0 then t else mk_case_term ctxt (p - 1) qs' c
    3.13