modified predicate compiler further to support tuples
authorbulwahn
Wed Sep 23 16:20:12 2009 +0200 (2009-09-23)
changeset 326645d4f32b02450
parent 32663 c2f63118b251
child 32665 8bf46a97ff79
modified predicate compiler further to support tuples
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 @@ -44,9 +44,9 @@
     1.4    (* temporary for testing of the compilation *)
     1.5    datatype indprem = Prem of term list * term | Negprem of term list * term | Sidecond of term |
     1.6      GeneratorPrem of term list * term | Generator of (string * typ);
     1.7 -  val prepare_intrs: theory -> string list ->
     1.8 + (* val prepare_intrs: theory -> string list ->
     1.9      (string * typ) list * int * string list * string list * (string * mode list) list *
    1.10 -    (string * (term list * indprem list) list) list * (string * (int option list * int)) list
    1.11 +    (string * (term list * indprem list) list) list * (string * (int option list * int)) list*)
    1.12    datatype compilation_funs = CompilationFuns of {
    1.13      mk_predT : typ -> typ,
    1.14      dest_predT : typ -> typ,
    1.15 @@ -61,12 +61,14 @@
    1.16    };  
    1.17    type moded_clause = term list * (indprem * tmode) list
    1.18    type 'a pred_mode_table = (string * (mode * 'a) list) list
    1.19 -  val infer_modes : bool -> theory -> (string * mode list) list
    1.20 -    -> (string * (int option list * int)) list -> string list
    1.21 +  val infer_modes : theory -> (string * mode list) list
    1.22 +    -> (string * mode list) list
    1.23 +    -> string list
    1.24      -> (string * (term list * indprem list) list) list
    1.25      -> (moded_clause list) pred_mode_table
    1.26 -  val infer_modes_with_generator : theory -> (string * (int list option list * int list) list) list
    1.27 -    -> (string * (int option list * int)) list -> string list
    1.28 +  val infer_modes_with_generator : theory -> (string * mode list) list
    1.29 +    -> (string * mode list) list
    1.30 +    -> string list
    1.31      -> (string * (term list * indprem list) list) list
    1.32      -> (moded_clause list) pred_mode_table  
    1.33    (*val compile_preds : theory -> compilation_funs -> string list -> string list
    1.34 @@ -98,6 +100,7 @@
    1.35    val is_constrt : theory -> term -> bool
    1.36    val is_predT : typ -> bool
    1.37    val guess_nparams : typ -> int
    1.38 +  val cprods_subset : 'a list list -> 'a list list
    1.39  end;
    1.40  
    1.41  structure Predicate_Compile : PREDICATE_COMPILE =
    1.42 @@ -866,7 +869,11 @@
    1.43  
    1.44  fun cprods xss = foldr (map op :: o cprod) [[]] xss;
    1.45  
    1.46 -
    1.47 +fun cprods_subset [] = [[]]
    1.48 +  | cprods_subset (xs :: xss) =
    1.49 +  let
    1.50 +    val yss = (cprods_subset xss)
    1.51 +  in maps (fn ys => map (fn x => cons x ys) xs) yss @ yss end
    1.52    
    1.53  (*TODO: cleanup function and put together with modes_of_term *)
    1.54  (*
    1.55 @@ -1036,8 +1043,8 @@
    1.56      else NONE
    1.57    end;
    1.58  
    1.59 -fun check_modes_pred with_generator thy param_vs preds modes gen_modes (p, ms) =
    1.60 -  let val SOME rs = AList.lookup (op =) preds p
    1.61 +fun check_modes_pred with_generator thy param_vs clauses modes gen_modes (p, ms) =
    1.62 +  let val SOME rs = AList.lookup (op =) clauses p
    1.63    in (p, List.filter (fn m => case find_index
    1.64      (is_none o check_mode_clause with_generator thy param_vs modes gen_modes m) rs of
    1.65        ~1 => true
    1.66 @@ -1046,9 +1053,9 @@
    1.67          Output.tracing (commas (map (Syntax.string_of_term_global thy) (fst (nth rs i)))); false)) ms)
    1.68    end;
    1.69  
    1.70 -fun get_modes_pred with_generator thy param_vs preds modes gen_modes (p, ms) =
    1.71 +fun get_modes_pred with_generator thy param_vs clauses modes gen_modes (p, ms) =
    1.72    let
    1.73 -    val SOME rs = AList.lookup (op =) preds p 
    1.74 +    val SOME rs = AList.lookup (op =) clauses p 
    1.75    in
    1.76      (p, map (fn m =>
    1.77        (m, map (the o check_mode_clause with_generator thy param_vs modes gen_modes m) rs)) ms)
    1.78 @@ -1058,20 +1065,14 @@
    1.79    let val y = f x
    1.80    in if x = y then x else fixp f y end;
    1.81  
    1.82 -fun modes_of_arities arities =
    1.83 -  (map (fn (s, (ks, k)) => (s, cprod (cprods (map
    1.84 -            (fn NONE => [NONE]
    1.85 -              | SOME k' => map SOME (map (map (rpair NONE)) (subsets 1 k'))) ks),
    1.86 -    map (map (rpair NONE)) (subsets 1 k)))) arities)
    1.87 -  
    1.88 -fun infer_modes with_generator thy extra_modes arities param_vs preds =
    1.89 +fun infer_modes thy extra_modes all_modes param_vs clauses =
    1.90    let
    1.91      val modes =
    1.92        fixp (fn modes =>
    1.93 -        map (check_modes_pred with_generator thy param_vs preds (modes @ extra_modes) []) modes)
    1.94 -          (modes_of_arities arities)
    1.95 +        map (check_modes_pred false thy param_vs clauses (modes @ extra_modes) []) modes)
    1.96 +          all_modes
    1.97    in
    1.98 -    map (get_modes_pred with_generator thy param_vs preds (modes @ extra_modes) []) modes
    1.99 +    map (get_modes_pred false thy param_vs clauses (modes @ extra_modes) []) modes
   1.100    end;
   1.101  
   1.102  fun remove_from rem [] = []
   1.103 @@ -1081,19 +1082,19 @@
   1.104      | SOME vs' => (k, vs \\ vs'))
   1.105      :: remove_from rem xs
   1.106      
   1.107 -fun infer_modes_with_generator thy extra_modes arities param_vs preds =
   1.108 +fun infer_modes_with_generator thy extra_modes all_modes param_vs clauses =
   1.109    let
   1.110 -    val prednames = map fst preds
   1.111 +    val prednames = map fst clauses
   1.112      val extra_modes = all_modes_of thy
   1.113      val gen_modes = all_generator_modes_of thy
   1.114        |> filter_out (fn (name, _) => member (op =) prednames name)
   1.115 -    val starting_modes = remove_from extra_modes (modes_of_arities arities) 
   1.116 +    val starting_modes = remove_from extra_modes all_modes 
   1.117      val modes =
   1.118        fixp (fn modes =>
   1.119 -        map (check_modes_pred true thy param_vs preds extra_modes (gen_modes @ modes)) modes)
   1.120 +        map (check_modes_pred true thy param_vs clauses extra_modes (gen_modes @ modes)) modes)
   1.121           starting_modes 
   1.122    in
   1.123 -    map (get_modes_pred true thy param_vs preds extra_modes (gen_modes @ modes)) modes
   1.124 +    map (get_modes_pred true thy param_vs clauses extra_modes (gen_modes @ modes)) modes
   1.125    end;
   1.126  
   1.127  (* term construction *)
   1.128 @@ -1430,7 +1431,8 @@
   1.129  fun create_constname_of_mode thy prefix name mode = 
   1.130    let
   1.131      fun string_of_mode mode = if null mode then "0"
   1.132 -      else space_implode "_" (map (fn (i, NONE) => string_of_int i | (i, SOME _) => error "pair mode") mode)
   1.133 +      else space_implode "_" (map (fn (i, NONE) => string_of_int i | (i, SOME pis) => string_of_int i ^ "p"
   1.134 +        ^ space_implode "p" (map string_of_int pis)) mode)
   1.135      val HOmode = space_implode "_and_"
   1.136        (fold (fn NONE => I | SOME mode => cons (string_of_mode mode)) (fst mode) [])
   1.137    in
   1.138 @@ -1952,17 +1954,38 @@
   1.139               length Us)) arities)
   1.140      end;
   1.141      val (clauses, arities) = fold add_clause intrs ([], []);
   1.142 -  in (preds, nparams, all_vs, param_vs, extra_modes, clauses, arities) end;
   1.143 +    fun modes_of_arities arities =
   1.144 +      (map (fn (s, (ks, k)) => (s, cprod (cprods (map
   1.145 +            (fn NONE => [NONE]
   1.146 +              | SOME k' => map SOME (map (map (rpair NONE)) (subsets 1 k'))) ks),
   1.147 +       map (map (rpair NONE)) (subsets 1 k)))) arities)
   1.148 +    fun modes_of_typ T =
   1.149 +      let
   1.150 +        val (Ts, Us) = chop nparams (binder_types T)
   1.151 +        fun all_smodes_of_typs Ts = cprods_subset (
   1.152 +          map_index (fn (i, U) =>
   1.153 +            case HOLogic.strip_tupleT U of
   1.154 +              [] => [(i + 1, NONE)]
   1.155 +            | [U] => [(i + 1, NONE)]
   1.156 +            | Us =>  map (pair (i + 1) o SOME) (subsets 1 (length Us)))
   1.157 +          Ts)
   1.158 +      in
   1.159 +        cprod (cprods (map (fn T => case strip_type T of
   1.160 +          (Rs as _ :: _, Type ("bool", [])) => map SOME (all_smodes_of_typs Rs) | _ => [NONE]) Ts),
   1.161 +           all_smodes_of_typs Us)
   1.162 +      end
   1.163 +    val all_modes = map (fn (s, T) => (s, modes_of_typ T)) preds
   1.164 +  in (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) end;
   1.165  
   1.166  (** main function of predicate compiler **)
   1.167  
   1.168  fun add_equations_of steps prednames thy =
   1.169    let
   1.170      val _ = Output.tracing ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
   1.171 -    val (preds, nparams, all_vs, param_vs, extra_modes, clauses, arities) =
   1.172 +    val (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) =
   1.173        prepare_intrs thy prednames
   1.174      val _ = Output.tracing "Infering modes..."
   1.175 -    val moded_clauses = #infer_modes steps thy extra_modes arities param_vs clauses 
   1.176 +    val moded_clauses = #infer_modes steps thy extra_modes all_modes param_vs clauses 
   1.177      val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
   1.178      val _ = print_modes modes
   1.179      val _ = print_moded_clauses thy moded_clauses
   1.180 @@ -2018,7 +2041,7 @@
   1.181  (* different instantiantions of the predicate compiler *)
   1.182  
   1.183  val add_equations = gen_add_equations
   1.184 -  {infer_modes = infer_modes false,
   1.185 +  {infer_modes = infer_modes,
   1.186    create_definitions = create_definitions,
   1.187    compile_preds = compile_preds PredicateCompFuns.compfuns mk_fun_of false,
   1.188    prove = prove,
   1.189 @@ -2026,7 +2049,7 @@
   1.190    qname = "equation"}
   1.191  
   1.192  val add_sizelim_equations = gen_add_equations
   1.193 -  {infer_modes = infer_modes false,
   1.194 +  {infer_modes = infer_modes,
   1.195    create_definitions = sizelim_create_definitions,
   1.196    compile_preds = compile_preds PredicateCompFuns.compfuns mk_sizelim_fun_of true,
   1.197    prove = prove_by_skip,