changed preprocessing due to problems with LightweightJava; added transfer of thereoms; changed the type of mode to support tuples in the predicate compiler
authorbulwahn
Wed Sep 23 16:20:12 2009 +0200 (2009-09-23)
changeset 32663c2f63118b251
parent 32662 2faf1148c062
child 32664 5d4f32b02450
changed preprocessing due to problems with LightweightJava; added transfer of thereoms; changed the type of mode to support tuples in the predicate compiler
src/HOL/ex/predicate_compile.ML
     1.1 --- a/src/HOL/ex/predicate_compile.ML	Wed Sep 23 16:20:12 2009 +0200
     1.2 +++ b/src/HOL/ex/predicate_compile.ML	Wed Sep 23 16:20:12 2009 +0200
     1.3 @@ -6,7 +6,9 @@
     1.4  
     1.5  signature PREDICATE_COMPILE =
     1.6  sig
     1.7 -  type mode = int list option list * int list
     1.8 +  type smode = (int * int list option) list
     1.9 +  type mode = smode option list * smode
    1.10 +  datatype tmode = Mode of mode * smode * tmode option list;
    1.11    (*val add_equations_of: bool -> string list -> theory -> theory *)
    1.12    val register_predicate : (thm list * thm * int) -> theory -> theory
    1.13    val is_registered : theory -> string -> bool
    1.14 @@ -57,10 +59,9 @@
    1.15      mk_map : typ -> typ -> term -> term -> term,
    1.16      lift_pred : term -> term
    1.17    };  
    1.18 -  datatype tmode = Mode of mode * int list * tmode option list;
    1.19    type moded_clause = term list * (indprem * tmode) list
    1.20    type 'a pred_mode_table = (string * (mode * 'a) list) list
    1.21 -  val infer_modes : bool -> theory -> (string * (int list option list * int list) list) list
    1.22 +  val infer_modes : bool -> theory -> (string * mode list) list
    1.23      -> (string * (int option list * int)) list -> string list
    1.24      -> (string * (term list * indprem list) list) list
    1.25      -> (moded_clause list) pred_mode_table
    1.26 @@ -183,25 +184,51 @@
    1.27  
    1.28  (** data structures **)
    1.29  
    1.30 -type smode = int list;
    1.31 +type smode = (int * int list option) list;
    1.32  type mode = smode option list * smode;
    1.33 -datatype tmode = Mode of mode * int list * tmode option list;
    1.34 +datatype tmode = Mode of mode * smode * tmode option list;
    1.35  
    1.36 -fun split_smode is ts =
    1.37 +fun gen_split_smode (mk_tuple, strip_tuple) smode ts =
    1.38    let
    1.39 +    fun split_tuple' _ _ [] = ([], [])
    1.40 +    | split_tuple' is i (t::ts) =
    1.41 +      (if i mem is then apfst else apsnd) (cons t)
    1.42 +        (split_tuple' is (i+1) ts)
    1.43 +    fun split_tuple is t = split_tuple' is 1 (strip_tuple t)
    1.44      fun split_smode' _ _ [] = ([], [])
    1.45 -      | split_smode' is i (t::ts) = (if i mem is then apfst else apsnd) (cons t)
    1.46 -          (split_smode' is (i+1) ts)
    1.47 -  in split_smode' is 1 ts end
    1.48 +      | split_smode' smode i (t::ts) =
    1.49 +        (if i mem (map fst smode) then
    1.50 +          case (the (AList.lookup (op =) smode i)) of
    1.51 +            NONE => apfst (cons t)
    1.52 +            | SOME is =>
    1.53 +              let
    1.54 +                val (ts1, ts2) = split_tuple is t
    1.55 +                fun cons_tuple ts = if null ts then I else cons (mk_tuple ts)
    1.56 +                in (apfst (cons_tuple ts1)) o (apsnd (cons_tuple ts2)) end
    1.57 +          else apsnd (cons t))
    1.58 +        (split_smode' smode (i+1) ts)
    1.59 +  in split_smode' smode 1 ts end
    1.60  
    1.61 -fun split_mode (iss, is) ts =
    1.62 +val split_smode = gen_split_smode (HOLogic.mk_tuple, HOLogic.strip_tuple)   
    1.63 +val split_smodeT = gen_split_smode (HOLogic.mk_tupleT, HOLogic.strip_tupleT)
    1.64 +
    1.65 +fun gen_split_mode split_smode (iss, is) ts =
    1.66    let
    1.67      val (t1, t2) = chop (length iss) ts 
    1.68    in (t1, split_smode is t2) end
    1.69  
    1.70 +val split_mode = gen_split_mode split_smode
    1.71 +val split_modeT = gen_split_mode split_smodeT
    1.72 +
    1.73 +fun string_of_smode js =
    1.74 +    commas (map
    1.75 +      (fn (i, is) =>
    1.76 +        string_of_int i ^ (case is of NONE => ""
    1.77 +    | SOME is => "p" ^ enclose "[" "]" (commas (map string_of_int is)))) js)
    1.78 +
    1.79  fun string_of_mode (iss, is) = space_implode " -> " (map
    1.80    (fn NONE => "X"
    1.81 -    | SOME js => enclose "[" "]" (commas (map string_of_int js)))
    1.82 +    | SOME js => enclose "[" "]" (string_of_smode js))
    1.83         (iss @ [SOME is]));
    1.84  
    1.85  fun string_of_tmode (Mode (predmode, termmode, param_modes)) =
    1.86 @@ -282,11 +309,11 @@
    1.87  
    1.88  val all_preds_of = Graph.keys o PredData.get
    1.89  
    1.90 -val intros_of = #intros oo the_pred_data
    1.91 +fun intros_of thy = map (Thm.transfer thy) o #intros o the_pred_data thy
    1.92  
    1.93  fun the_elim_of thy name = case #elim (the_pred_data thy name)
    1.94   of NONE => error ("No elimination rule for predicate " ^ quote name)
    1.95 -  | SOME thm => thm 
    1.96 +  | SOME thm => Thm.transfer thy thm 
    1.97    
    1.98  val has_elim = is_some o #elim oo the_pred_data;
    1.99  
   1.100 @@ -367,10 +394,10 @@
   1.101      "Generator for " ^ v ^ " of Type " ^ (Syntax.string_of_typ_global thy T)
   1.102    | string_of_moded_prem thy (Negprem (ts, p), Mode (_, is, _)) =
   1.103      (Syntax.string_of_term_global thy (list_comb (p, ts))) ^
   1.104 -    "(negative mode: " ^ (space_implode ", " (map string_of_int is)) ^ ")"
   1.105 +    "(negative mode: " ^ string_of_smode is ^ ")"
   1.106    | string_of_moded_prem thy (Sidecond t, Mode (_, is, _)) =
   1.107      (Syntax.string_of_term_global thy t) ^
   1.108 -    "(sidecond mode: " ^ (space_implode ", " (map string_of_int is)) ^ ")"    
   1.109 +    "(sidecond mode: " ^ string_of_smode is ^ ")"    
   1.110    | string_of_moded_prem _ _ = error "string_of_moded_prem: unimplemented"
   1.111       
   1.112  fun print_moded_clauses thy =
   1.113 @@ -435,6 +462,8 @@
   1.114  
   1.115  fun preprocess_elim thy nparams elimrule =
   1.116    let
   1.117 +    val _ = Output.tracing ("Preprocessing elimination rule "
   1.118 +      ^ (Display.string_of_thm_global thy elimrule))
   1.119      fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) =
   1.120         HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
   1.121       | replace_eqs t = t
   1.122 @@ -450,11 +479,21 @@
   1.123       end 
   1.124      val cases' = map preprocess_case (tl prems)
   1.125      val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule)
   1.126 +    (*
   1.127 +    (*val _ =  Output.tracing ("elimrule': "^ (Syntax.string_of_term_global thy elimrule'))*)
   1.128 +    val bigeq = (Thm.symmetric (Conv.implies_concl_conv (MetaSimplifier.rewrite true [@{thm Predicate.eq_is_eq}])
   1.129 +         (cterm_of thy elimrule')))
   1.130 +    val _ = Output.tracing ("bigeq:" ^ (Display.string_of_thm_global thy bigeq))   
   1.131 +    val res = 
   1.132 +    Thm.equal_elim bigeq
   1.133 +      
   1.134 +      elimrule
   1.135 +    *)
   1.136 +    val t = (fn {...} => mycheat_tac thy 1)
   1.137 +    val eq = Goal.prove (ProofContext.init thy) [] [] (Logic.mk_equals ((Thm.prop_of elimrule), elimrule')) t
   1.138 +    val _ = Output.tracing "Preprocessed elimination rule"
   1.139    in
   1.140 -    Thm.equal_elim
   1.141 -      (Thm.symmetric (Conv.implies_concl_conv (MetaSimplifier.rewrite true [@{thm eq_is_eq}])
   1.142 -         (cterm_of thy elimrule')))
   1.143 -      elimrule
   1.144 +    Thm.equal_elim eq elimrule
   1.145    end;
   1.146  
   1.147  (* special case: predicate with no introduction rule *)
   1.148 @@ -629,7 +668,7 @@
   1.149  fun funT_of compfuns (iss, is) T =
   1.150    let
   1.151      val Ts = binder_types T
   1.152 -    val (paramTs, (inargTs, outargTs)) = split_mode (iss, is) Ts
   1.153 +    val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts
   1.154      val paramTs' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) iss paramTs 
   1.155    in
   1.156      (paramTs' @ inargTs) ---> (mk_predT compfuns (mk_tupleT outargTs))
   1.157 @@ -638,7 +677,7 @@
   1.158  fun sizelim_funT_of compfuns (iss, is) T =
   1.159    let
   1.160      val Ts = binder_types T
   1.161 -    val (paramTs, (inargTs, outargTs)) = split_mode (iss, is) Ts
   1.162 +    val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts
   1.163      val paramTs' = map2 (fn SOME is => sizelim_funT_of compfuns ([], is) | NONE => I) iss paramTs 
   1.164    in
   1.165      (paramTs' @ inargTs @ [@{typ "code_numeral"}]) ---> (mk_predT compfuns (mk_tupleT outargTs))
   1.166 @@ -868,7 +907,7 @@
   1.167  *)
   1.168  fun modes_of_term modes t =
   1.169    let
   1.170 -    val ks = 1 upto length (binder_types (fastype_of t));
   1.171 +    val ks = map_index (fn (i, T) => (i, NONE)) (binder_types (fastype_of t));
   1.172      val default = [Mode (([], ks), ks, [])];
   1.173      fun mk_modes name args = Option.map (maps (fn (m as (iss, is)) =>
   1.174          let
   1.175 @@ -877,10 +916,10 @@
   1.176                error ("Too few arguments for inductive predicate " ^ name)
   1.177              else chop (length iss) args;
   1.178            val k = length args2;
   1.179 -          val prfx = 1 upto k
   1.180 +          val prfx = map (rpair NONE) (1 upto k)
   1.181          in
   1.182            if not (is_prefix op = prfx is) then [] else
   1.183 -          let val is' = map (fn i => i - k) (List.drop (is, k))
   1.184 +          let val is' = List.drop (is, k)
   1.185            in map (fn x => Mode (m, is', x)) (cprods (map
   1.186              (fn (NONE, _) => [NONE]
   1.187                | (SOME js, arg) => map SOME (filter
   1.188 @@ -1003,7 +1042,8 @@
   1.189      (is_none o check_mode_clause with_generator thy param_vs modes gen_modes m) rs of
   1.190        ~1 => true
   1.191      | i => (Output.tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
   1.192 -      p ^ " violates mode " ^ string_of_mode m); false)) ms)
   1.193 +      p ^ " violates mode " ^ string_of_mode m);
   1.194 +        Output.tracing (commas (map (Syntax.string_of_term_global thy) (fst (nth rs i)))); false)) ms)
   1.195    end;
   1.196  
   1.197  fun get_modes_pred with_generator thy param_vs preds modes gen_modes (p, ms) =
   1.198 @@ -1021,8 +1061,8 @@
   1.199  fun modes_of_arities arities =
   1.200    (map (fn (s, (ks, k)) => (s, cprod (cprods (map
   1.201              (fn NONE => [NONE]
   1.202 -              | SOME k' => map SOME (subsets 1 k')) ks),
   1.203 -            subsets 1 k))) arities)
   1.204 +              | SOME k' => map SOME (map (map (rpair NONE)) (subsets 1 k'))) ks),
   1.205 +    map (map (rpair NONE)) (subsets 1 k)))) arities)
   1.206    
   1.207  fun infer_modes with_generator thy extra_modes arities param_vs preds =
   1.208    let
   1.209 @@ -1294,11 +1334,11 @@
   1.210  
   1.211  fun compile_pred compfuns mk_fun_of use_size thy all_vs param_vs s T mode moded_cls =
   1.212    let
   1.213 -    val (Ts1, (Us1, Us2)) = split_mode mode (binder_types T)
   1.214 +    val (Ts1, (Us1, Us2)) = split_modeT mode (binder_types T)
   1.215      val funT_of = if use_size then sizelim_funT_of else funT_of 
   1.216      val Ts1' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) (fst mode) Ts1
   1.217      val xnames = Name.variant_list (all_vs @ param_vs)
   1.218 -      (map (fn i => "x" ^ string_of_int i) (snd mode));
   1.219 +      (map (fn (i, NONE) => "x" ^ string_of_int i | (i, SOME s) => error "pair mode") (snd mode));
   1.220      val size_name = Name.variant (all_vs @ param_vs @ xnames) "size"
   1.221      (* termify code: val xs = map2 (fn s => fn T => Free (s, termifyT T)) xnames Us1; *)
   1.222      val xs = map2 (fn s => fn T => Free (s, T)) xnames Us1;
   1.223 @@ -1390,7 +1430,7 @@
   1.224  fun create_constname_of_mode thy prefix name mode = 
   1.225    let
   1.226      fun string_of_mode mode = if null mode then "0"
   1.227 -      else space_implode "_" (map string_of_int mode)
   1.228 +      else space_implode "_" (map (fn (i, NONE) => string_of_int i | (i, SOME _) => error "pair mode") mode)
   1.229      val HOmode = space_implode "_and_"
   1.230        (fold (fn NONE => I | SOME mode => cons (string_of_mode mode)) (fst mode) [])
   1.231    in
   1.232 @@ -1407,14 +1447,14 @@
   1.233        val mode_cbasename = Long_Name.base_name mode_cname
   1.234        val Ts = binder_types T
   1.235        val (Ts1, Ts2) = chop (length iss) Ts
   1.236 -      val (Us1, Us2) =  split_smode is Ts2
   1.237 +      val (Us1, Us2) =  split_smodeT is Ts2
   1.238        val Ts1' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) iss Ts1
   1.239        val funT = (Ts1' @ Us1) ---> (mk_predT compfuns (mk_tupleT Us2))
   1.240        val names = Name.variant_list []
   1.241          (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
   1.242 -      val xs = map Free (names ~~ (Ts1' @ Ts2));                   
   1.243 -      val (xparams, xargs) = chop (length iss) xs;
   1.244 -      val (xins, xouts) = split_smode is xargs 
   1.245 +      val xs = map Free (names ~~ (Ts1' @ Ts2))
   1.246 +      val (xparams, xargs) = chop (length iss) xs
   1.247 +      val (xins, xouts) = split_smode is xargs
   1.248        val (xparams', names') = fold_map mk_Eval_of ((xparams ~~ Ts1) ~~ iss) names
   1.249        fun mk_split_lambda [] t = lambda (Free (Name.variant names' "x", HOLogic.unitT)) t
   1.250          | mk_split_lambda [x] t = lambda x t
   1.251 @@ -1572,7 +1612,8 @@
   1.252        | _ => nameTs
   1.253      val preds = preds_of t []
   1.254      val defs = map
   1.255 -      (fn (pred, T) => predfun_definition_of thy pred ([], (1 upto (length (binder_types T)))))
   1.256 +      (fn (pred, T) => predfun_definition_of thy pred
   1.257 +        ([], map (rpair NONE) (1 upto (length (binder_types T)))))
   1.258          preds
   1.259    in 
   1.260      (* remove not_False_eq_True when simpset in prove_match is better *)
   1.261 @@ -1734,7 +1775,8 @@
   1.262      | _ => nameTs
   1.263    val preds = preds_of t []
   1.264    val defs = map
   1.265 -    (fn (pred, T) => predfun_definition_of thy pred ([], (1 upto (length (binder_types T)))))
   1.266 +    (fn (pred, T) => predfun_definition_of thy pred 
   1.267 +      ([], map (rpair NONE) (1 upto (length (binder_types T)))))
   1.268        preds
   1.269    in
   1.270     (* only simplify the one assumption *)
   1.271 @@ -1991,7 +2033,7 @@
   1.272    are_not_defined = (fn thy => fn preds => true), (* TODO *)
   1.273    qname = "sizelim_equation"
   1.274    }
   1.275 -  
   1.276 +
   1.277  val add_quickcheck_equations = gen_add_equations
   1.278    {infer_modes = infer_modes_with_generator,
   1.279    create_definitions = rpred_create_definitions,
   1.280 @@ -2036,7 +2078,6 @@
   1.281  local
   1.282  
   1.283  (* TODO: make TheoryDataFun to GenericDataFun & remove duplication of local theory and theory *)
   1.284 -(* TODO: must create state to prove multiple cases *)
   1.285  fun generic_code_pred prep_const raw_const lthy =
   1.286    let
   1.287      val thy = ProofContext.theory_of lthy
   1.288 @@ -2114,7 +2155,8 @@
   1.289      val user_mode = map_filter I (map_index
   1.290        (fn (i, t) => case t of Bound j => if j < length Ts then NONE
   1.291          else SOME (i+1) | _ => SOME (i+1)) args); (*FIXME dangling bounds should not occur*)
   1.292 -    val modes = filter (fn Mode (_, is, _) => is = user_mode)
   1.293 +    val user_mode' = map (rpair NONE) user_mode
   1.294 +    val modes = filter (fn Mode (_, is, _) => is = user_mode')
   1.295        (modes_of_term (all_modes_of thy) (list_comb (pred, params)));
   1.296      val m = case modes
   1.297       of [] => error ("No mode possible for comprehension "
   1.298 @@ -2122,7 +2164,7 @@
   1.299        | [m] => m
   1.300        | m :: _ :: _ => (warning ("Multiple modes possible for comprehension "
   1.301                  ^ Syntax.string_of_term_global thy t_compr); m);
   1.302 -    val (inargs, outargs) = split_smode user_mode args;
   1.303 +    val (inargs, outargs) = split_smode user_mode' args;
   1.304      val t_pred = list_comb (compile_expr NONE thy (m, list_comb (pred, params)), inargs);
   1.305      val t_eval = if null outargs then t_pred else let
   1.306          val outargs_bounds = map (fn Bound i => i) outargs;