proposed modes for code_pred now supports modes for mutual predicates
authorbulwahn
Wed Sep 15 09:36:38 2010 +0200 (2010-09-15)
changeset 39382c797f3ab2ae1
parent 39381 9717ea8d42b3
child 39383 ddfafa97da2f
proposed modes for code_pred now supports modes for mutual predicates
src/HOL/Tools/Predicate_Compile/predicate_compile.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Sep 15 08:58:34 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Sep 15 09:36:38 2010 +0200
     1.3 @@ -139,16 +139,24 @@
     1.4          (Term_Graph.strong_conn gr) thy))
     1.5    end
     1.6  
     1.7 -fun extract_options (((expected_modes, proposed_modes), (compilation, raw_options)), const) =
     1.8 +datatype proposed_modes = Multiple_Preds of (string * (mode * string option) list) list
     1.9 +  | Single_Pred of (mode * string option) list
    1.10 +
    1.11 +fun extract_options lthy (((expected_modes, proposed_modes), (compilation, raw_options)), const) =
    1.12    let
    1.13      fun chk s = member (op =) raw_options s
    1.14 +    val proposed_modes = case proposed_modes of
    1.15 +          Single_Pred proposed_modes => [(const, proposed_modes)]
    1.16 +        | Multiple_Preds proposed_modes => map
    1.17 +          (apfst (Code.read_const (ProofContext.theory_of lthy))) proposed_modes
    1.18    in
    1.19      Options {
    1.20        expected_modes = Option.map (pair const) expected_modes,
    1.21 -      proposed_modes = Option.map (pair const o map fst) proposed_modes,
    1.22 +      proposed_modes = 
    1.23 +        map (apsnd (map fst)) proposed_modes,
    1.24        proposed_names =
    1.25 -        the_default [] (Option.map (map_filter
    1.26 -          (fn (m, NONE) => NONE | (m, SOME name) => SOME ((const, m), name))) proposed_modes),
    1.27 +        maps (fn (predname, ms) => (map_filter
    1.28 +          (fn (m, NONE) => NONE | (m, SOME name) => SOME ((predname, m), name))) ms) proposed_modes,
    1.29        show_steps = chk "show_steps",
    1.30        show_intermediate_results = chk "show_intermediate_results",
    1.31        show_proof_trace = chk "show_proof_trace",
    1.32 @@ -174,7 +182,7 @@
    1.33       val const = Code.read_const thy raw_const
    1.34       val T = Sign.the_const_type thy const
    1.35       val t = Const (const, T)
    1.36 -     val options = extract_options (((expected_modes, proposed_modes), raw_options), const)
    1.37 +     val options = extract_options lthy (((expected_modes, proposed_modes), raw_options), const)
    1.38    in
    1.39      if is_inductify options then
    1.40        let
    1.41 @@ -208,9 +216,13 @@
    1.42  val mode_and_opt_proposal = parse_mode_expr --
    1.43    Scan.optional (Args.$$$ "as" |-- Parse.xname >> SOME) NONE
    1.44  
    1.45 +
    1.46  val opt_modes =
    1.47    Scan.optional (Parse.$$$ "(" |-- Args.$$$ "modes" |-- Parse.$$$ ":" |--
    1.48 -    Parse.enum "," mode_and_opt_proposal --| Parse.$$$ ")" >> SOME) NONE
    1.49 +    (((Parse.enum1 "and" (Parse.xname --| Parse.$$$ ":" --
    1.50 +        (Parse.enum "," mode_and_opt_proposal))) >> Multiple_Preds)
    1.51 +      || ((Parse.enum "," mode_and_opt_proposal) >> Single_Pred))
    1.52 +    --| Parse.$$$ ")") (Multiple_Preds [])
    1.53  
    1.54  val opt_expected_modes =
    1.55    Scan.optional (Parse.$$$ "(" |-- Args.$$$ "expected_modes" |-- Parse.$$$ ":" |--
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Sep 15 08:58:34 2010 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Sep 15 09:36:38 2010 +0200
     2.3 @@ -99,7 +99,7 @@
     2.4    (* Different options for compiler *)
     2.5    datatype options = Options of {  
     2.6      expected_modes : (string * mode list) option,
     2.7 -    proposed_modes : (string * mode list) option,
     2.8 +    proposed_modes : (string * mode list) list,
     2.9      proposed_names : ((string * mode) * string) list,
    2.10      show_steps : bool,
    2.11      show_proof_trace : bool,
    2.12 @@ -119,7 +119,7 @@
    2.13      compilation : compilation
    2.14    };
    2.15    val expected_modes : options -> (string * mode list) option
    2.16 -  val proposed_modes : options -> (string * mode list) option
    2.17 +  val proposed_modes : options -> string -> mode list option
    2.18    val proposed_names : options -> string -> mode -> string option
    2.19    val show_steps : options -> bool
    2.20    val show_proof_trace : options -> bool
    2.21 @@ -703,7 +703,7 @@
    2.22  
    2.23  datatype options = Options of {  
    2.24    expected_modes : (string * mode list) option,
    2.25 -  proposed_modes : (string * mode list) option,
    2.26 +  proposed_modes : (string * mode list) list,
    2.27    proposed_names : ((string * mode) * string) list,
    2.28    show_steps : bool,
    2.29    show_proof_trace : bool,
    2.30 @@ -724,7 +724,7 @@
    2.31  };
    2.32  
    2.33  fun expected_modes (Options opt) = #expected_modes opt
    2.34 -fun proposed_modes (Options opt) = #proposed_modes opt
    2.35 +fun proposed_modes (Options opt) = AList.lookup (op =) (#proposed_modes opt)
    2.36  fun proposed_names (Options opt) name mode = AList.lookup (eq_pair (op =) eq_mode)
    2.37    (#proposed_names opt) (name, mode)
    2.38  
    2.39 @@ -752,7 +752,7 @@
    2.40  
    2.41  val default_options = Options {
    2.42    expected_modes = NONE,
    2.43 -  proposed_modes = NONE,
    2.44 +  proposed_modes = [],
    2.45    proposed_names = [],
    2.46    show_steps = false,
    2.47    show_intermediate_results = false,
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Sep 15 08:58:34 2010 +0200
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Sep 15 09:36:38 2010 +0200
     3.3 @@ -400,8 +400,8 @@
     3.4    | NONE => ()
     3.5  
     3.6  fun check_proposed_modes preds options modes errors =
     3.7 -  case proposed_modes options of
     3.8 -    SOME (s, ms) => (case AList.lookup (op =) modes s of
     3.9 +  map (fn (s, _) => case proposed_modes options s of
    3.10 +    SOME ms => (case AList.lookup (op =) modes s of
    3.11        SOME inferred_ms =>
    3.12          let
    3.13            val preds_without_modes = map fst (filter (null o snd) modes)
    3.14 @@ -419,7 +419,7 @@
    3.15            else ()
    3.16          end
    3.17        | NONE => ())
    3.18 -  | NONE => ()
    3.19 +  | NONE => ()) preds
    3.20  
    3.21  (* importing introduction rules *)
    3.22  
    3.23 @@ -2700,8 +2700,8 @@
    3.24          all_modes_of_typ T
    3.25      val all_modes = 
    3.26        map (fn (s, T) =>
    3.27 -        (s, case (proposed_modes options) of
    3.28 -            SOME (s', ms) => if s = s' then ms else generate_modes s T
    3.29 +        (s, case proposed_modes options s of
    3.30 +            SOME ms => ms
    3.31            | NONE => generate_modes s T)) preds
    3.32      val params =
    3.33        case intrs of
    3.34 @@ -2719,7 +2719,7 @@
    3.35          let
    3.36            val (p, args) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr)) 
    3.37          in
    3.38 -          ho_args_of (hd (the (AList.lookup (op =) all_modes (fst (dest_Const p))))) args
    3.39 +          ho_args_of_typ (snd (dest_Const p)) args
    3.40          end
    3.41      val param_vs = map (fst o dest_Free) params
    3.42      fun add_clause intr clauses =
     4.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Sep 15 08:58:34 2010 +0200
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Sep 15 09:36:38 2010 +0200
     4.3 @@ -56,7 +56,7 @@
     4.4  
     4.5  val options = Options {
     4.6    expected_modes = NONE,
     4.7 -  proposed_modes = NONE,
     4.8 +  proposed_modes = [],
     4.9    proposed_names = [],
    4.10    show_steps = false,
    4.11    show_intermediate_results = false,