ported to use new-style datatypes
authorblanchet
Mon Sep 01 18:42:02 2014 +0200 (2014-09-01)
changeset 581305e9170812356
parent 58129 3ec65a7f2b50
child 58131 1abeda3c3bc2
ported to use new-style datatypes
* * *
compile
src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy
src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy
src/HOL/SPARK/Examples/Sqrt/Sqrt.thy
src/HOL/SPARK/Manual/Complex_Types.thy
src/HOL/SPARK/Manual/Proc1.thy
src/HOL/SPARK/Manual/Proc2.thy
src/HOL/SPARK/Manual/Reference.thy
src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy
src/HOL/SPARK/Tools/spark_vcs.ML
src/HOL/Tools/BNF/bnf_lfp_compat.ML
     1.1 --- a/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Mon Sep 01 17:34:03 2014 +0200
     1.2 +++ b/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Mon Sep 01 18:42:02 2014 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4  *)
     1.5  
     1.6  theory Greatest_Common_Divisor
     1.7 -imports SPARK GCD
     1.8 +imports "../../SPARK" GCD
     1.9  begin
    1.10  
    1.11  spark_proof_functions
     2.1 --- a/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy	Mon Sep 01 17:34:03 2014 +0200
     2.2 +++ b/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy	Mon Sep 01 18:42:02 2014 +0200
     2.3 @@ -4,7 +4,7 @@
     2.4  *)
     2.5  
     2.6  theory Longest_Increasing_Subsequence
     2.7 -imports SPARK
     2.8 +imports "../../SPARK"
     2.9  begin
    2.10  
    2.11  text {*
     3.1 --- a/src/HOL/SPARK/Examples/Sqrt/Sqrt.thy	Mon Sep 01 17:34:03 2014 +0200
     3.2 +++ b/src/HOL/SPARK/Examples/Sqrt/Sqrt.thy	Mon Sep 01 18:42:02 2014 +0200
     3.3 @@ -4,7 +4,7 @@
     3.4  *)
     3.5  
     3.6  theory Sqrt
     3.7 -imports SPARK
     3.8 +imports "../../SPARK"
     3.9  begin
    3.10  
    3.11  spark_open "sqrt/isqrt"
     4.1 --- a/src/HOL/SPARK/Manual/Complex_Types.thy	Mon Sep 01 17:34:03 2014 +0200
     4.2 +++ b/src/HOL/SPARK/Manual/Complex_Types.thy	Mon Sep 01 18:42:02 2014 +0200
     4.3 @@ -1,8 +1,8 @@
     4.4  theory Complex_Types
     4.5 -imports SPARK
     4.6 +imports "../SPARK"
     4.7  begin
     4.8  
     4.9 -datatype day = Mon | Tue | Wed | Thu | Fri | Sat | Sun
    4.10 +datatype_new day = Mon | Tue | Wed | Thu | Fri | Sat | Sun
    4.11  
    4.12  record two_fields =
    4.13    Field1 :: "int \<times> day \<Rightarrow> int"
     5.1 --- a/src/HOL/SPARK/Manual/Proc1.thy	Mon Sep 01 17:34:03 2014 +0200
     5.2 +++ b/src/HOL/SPARK/Manual/Proc1.thy	Mon Sep 01 18:42:02 2014 +0200
     5.3 @@ -1,5 +1,5 @@
     5.4  theory Proc1
     5.5 -imports SPARK
     5.6 +imports "../SPARK"
     5.7  begin
     5.8  
     5.9  spark_open "loop_invariant/proc1"
     6.1 --- a/src/HOL/SPARK/Manual/Proc2.thy	Mon Sep 01 17:34:03 2014 +0200
     6.2 +++ b/src/HOL/SPARK/Manual/Proc2.thy	Mon Sep 01 18:42:02 2014 +0200
     6.3 @@ -1,5 +1,5 @@
     6.4  theory Proc2
     6.5 -imports SPARK
     6.6 +imports "../SPARK"
     6.7  begin
     6.8  
     6.9  spark_open "loop_invariant/proc2"
     7.1 --- a/src/HOL/SPARK/Manual/Reference.thy	Mon Sep 01 17:34:03 2014 +0200
     7.2 +++ b/src/HOL/SPARK/Manual/Reference.thy	Mon Sep 01 18:42:02 2014 +0200
     7.3 @@ -1,6 +1,6 @@
     7.4  (*<*)
     7.5  theory Reference
     7.6 -imports SPARK
     7.7 +imports "../SPARK"
     7.8  begin
     7.9  
    7.10  syntax (my_constrain output)
     8.1 --- a/src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy	Mon Sep 01 17:34:03 2014 +0200
     8.2 +++ b/src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy	Mon Sep 01 18:42:02 2014 +0200
     8.3 @@ -4,7 +4,7 @@
     8.4  *)
     8.5  
     8.6  theory Simple_Greatest_Common_Divisor
     8.7 -imports SPARK GCD
     8.8 +imports "../SPARK" GCD
     8.9  begin
    8.10  
    8.11  spark_proof_functions
     9.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Mon Sep 01 17:34:03 2014 +0200
     9.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Mon Sep 01 18:42:02 2014 +0200
     9.3 @@ -173,8 +173,8 @@
     9.4  
     9.5  fun add_enum_type tyname tyname' thy =
     9.6    let
     9.7 -    val {case_name, ...} = the (Old_Datatype_Data.get_info thy tyname');
     9.8 -    val cs = map Const (the (Old_Datatype_Data.get_constrs thy tyname'));
     9.9 +    val {case_name, ...} = the (BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Keep_Nesting tyname');
    9.10 +    val cs = map Const (the (BNF_LFP_Compat.get_constrs thy tyname'));
    9.11      val k = length cs;
    9.12      val T = Type (tyname', []);
    9.13      val p = Const (@{const_name pos}, T --> HOLogic.intT);
    9.14 @@ -209,8 +209,8 @@
    9.15        (fn _ =>
    9.16           rtac @{thm subset_antisym} 1 THEN
    9.17           rtac @{thm subsetI} 1 THEN
    9.18 -         Old_Datatype_Aux.exh_tac (K (#exhaust (Old_Datatype_Data.the_info
    9.19 -           (Proof_Context.theory_of lthy) tyname'))) 1 THEN
    9.20 +         Old_Datatype_Aux.exh_tac (K (#exhaust (BNF_LFP_Compat.the_info
    9.21 +           (Proof_Context.theory_of lthy) BNF_LFP_Compat.Keep_Nesting tyname'))) 1 THEN
    9.22           ALLGOALS (asm_full_simp_tac lthy));
    9.23  
    9.24      val finite_UNIV = Goal.prove lthy [] []
    9.25 @@ -320,14 +320,14 @@
    9.26                  val tyname = Sign.full_name thy tyb
    9.27                in
    9.28                  (thy |>
    9.29 -                 Old_Datatype.add_datatype {strict = true, quiet = true}
    9.30 +                 BNF_LFP_Compat.add_datatype BNF_LFP_Compat.Keep_Nesting
    9.31                     [((tyb, [], NoSyn),
    9.32                       map (fn s => (Binding.name s, [], NoSyn)) els)] |> snd |>
    9.33                   add_enum_type s tyname,
    9.34                   tyname)
    9.35                end
    9.36            | SOME (T as Type (tyname, []), cmap) =>
    9.37 -              (case Old_Datatype_Data.get_constrs thy tyname of
    9.38 +              (case BNF_LFP_Compat.get_constrs thy tyname of
    9.39                   NONE => assoc_ty_err thy T s "is not a datatype"
    9.40                 | SOME cs =>
    9.41                     let val (prfx', _) = strip_prfx s
    9.42 @@ -338,7 +338,7 @@
    9.43                       | SOME msg => assoc_ty_err thy T s msg
    9.44                     end)
    9.45            | SOME (T, _) => assoc_ty_err thy T s "is not a datatype");
    9.46 -        val cs = map Const (the (Old_Datatype_Data.get_constrs thy' tyname));
    9.47 +        val cs = map Const (the (BNF_LFP_Compat.get_constrs thy' tyname));
    9.48        in
    9.49          ((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab,
    9.50            fold Name.declare els ctxt),
    9.51 @@ -888,7 +888,7 @@
    9.52                  handle Symtab.DUP _ => error ("SPARK type " ^ s ^
    9.53                    " already associated with type")) |>
    9.54          (fn thy' =>
    9.55 -           case Old_Datatype_Data.get_constrs thy' tyname of
    9.56 +           case BNF_LFP_Compat.get_constrs thy' tyname of
    9.57               NONE => (case get_record_info thy' T of
    9.58                 NONE => thy'
    9.59               | SOME {fields, ...} =>
    10.1 --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Sep 01 17:34:03 2014 +0200
    10.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Sep 01 18:42:02 2014 +0200
    10.3 @@ -203,7 +203,7 @@
    10.4    end;
    10.5  
    10.6  fun get_info_of_new_datatype thy nesting_pref T_name =
    10.7 -  let val lthy = Named_Target.theory_init thy in
    10.8 +  let val lthy = Proof_Context.init_global thy in
    10.9      AList.lookup (op =) (infos_of_new_datatype_mutual_cluster lthy nesting_pref T_name) T_name
   10.10    end;
   10.11