src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 45450 dc2236b19a3d
parent 44241 7943b69f0188
child 45461 130c90bb80b4
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Nov 11 08:32:44 2011 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Nov 11 08:32:45 2011 +0100
     1.3 @@ -90,8 +90,8 @@
     1.4    val funT_of : compilation_funs -> mode -> typ -> typ
     1.5    (* Different compilations *)
     1.6    datatype compilation = Pred | Depth_Limited | Random | Depth_Limited_Random | DSeq | Annotated
     1.7 -    | Pos_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq
     1.8 -    | Pos_Generator_DSeq | Neg_Generator_DSeq
     1.9 +    | Pos_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq 
    1.10 +    | Pos_Generator_DSeq | Neg_Generator_DSeq | Pos_Generator_CPS | Neg_Generator_CPS
    1.11    val negative_compilation_of : compilation -> compilation
    1.12    val compilation_for_polarity : bool -> compilation -> compilation
    1.13    val is_depth_limited_compilation : compilation -> bool 
    1.14 @@ -642,14 +642,16 @@
    1.15  
    1.16  datatype compilation = Pred | Depth_Limited | Random | Depth_Limited_Random | DSeq | Annotated
    1.17    | Pos_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq |
    1.18 -    Pos_Generator_DSeq | Neg_Generator_DSeq
    1.19 +    Pos_Generator_DSeq | Neg_Generator_DSeq | Pos_Generator_CPS | Neg_Generator_CPS
    1.20  
    1.21  fun negative_compilation_of Pos_Random_DSeq = Neg_Random_DSeq
    1.22    | negative_compilation_of Neg_Random_DSeq = Pos_Random_DSeq
    1.23    | negative_compilation_of New_Pos_Random_DSeq = New_Neg_Random_DSeq
    1.24    | negative_compilation_of New_Neg_Random_DSeq = New_Pos_Random_DSeq
    1.25    | negative_compilation_of Pos_Generator_DSeq = Neg_Generator_DSeq
    1.26 -  | negative_compilation_of Pos_Generator_DSeq = Pos_Generator_DSeq
    1.27 +  | negative_compilation_of Neg_Generator_DSeq = Pos_Generator_DSeq
    1.28 +  | negative_compilation_of Pos_Generator_CPS = Neg_Generator_CPS
    1.29 +  | negative_compilation_of Neg_Generator_CPS = Pos_Generator_CPS  
    1.30    | negative_compilation_of c = c
    1.31    
    1.32  fun compilation_for_polarity false Pos_Random_DSeq = Neg_Random_DSeq
    1.33 @@ -674,7 +676,9 @@
    1.34    | New_Neg_Random_DSeq => "new_neg_random_dseq"
    1.35    | Pos_Generator_DSeq => "pos_generator_dseq"
    1.36    | Neg_Generator_DSeq => "neg_generator_dseq"
    1.37 -
    1.38 +  | Pos_Generator_CPS => "pos_generator_cps"
    1.39 +  | Neg_Generator_CPS => "neg_generator_cps"
    1.40 +  
    1.41  val compilation_names = [("pred", Pred),
    1.42    ("random", Random),
    1.43    ("depth_limited", Depth_Limited),
    1.44 @@ -683,13 +687,14 @@
    1.45    ("dseq", DSeq),
    1.46    ("random_dseq", Pos_Random_DSeq),
    1.47    ("new_random_dseq", New_Pos_Random_DSeq),
    1.48 -  ("generator_dseq", Pos_Generator_DSeq)]
    1.49 +  ("generator_dseq", Pos_Generator_DSeq),
    1.50 +  ("generator_cps", Pos_Generator_CPS)]
    1.51  
    1.52  val non_random_compilations = [Pred, Depth_Limited, DSeq, Annotated]
    1.53  
    1.54  
    1.55  val random_compilations = [Random, Depth_Limited_Random,
    1.56 -  Pos_Random_DSeq, Neg_Random_DSeq, New_Pos_Random_DSeq, New_Neg_Random_DSeq]
    1.57 +  Pos_Random_DSeq, Neg_Random_DSeq, New_Pos_Random_DSeq, New_Neg_Random_DSeq, Pos_Generator_CPS]
    1.58  
    1.59  (* datastructures and setup for generic compilation *)
    1.60