src/HOL/Tools/smallvalue_generators.ML
changeset 41902 1941b3315952
parent 41901 45a79edbe73b
child 41903 39fd77f0ae59
equal deleted inserted replaced
41901:45a79edbe73b 41902:1941b3315952
   300   | dest_fun_upd t = raise TERM ("dest_fun_upd", [t])
   300   | dest_fun_upd t = raise TERM ("dest_fun_upd", [t])
   301 
   301 
   302 fun mk_fun_upd T1 T2 (t1, t2) t = 
   302 fun mk_fun_upd T1 T2 (t1, t2) t = 
   303   Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2) $ t $ t1 $ t2
   303   Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2) $ t $ t1 $ t2
   304 
   304 
   305 fun dest_plain_fun t =
   305 fun dest_fun_upds t =
   306   case try dest_fun_upd t of
   306   case try dest_fun_upd t of
   307     NONE =>
   307     NONE =>
   308       (case t of
   308       (case t of
   309         Abs (_, _, _) => ([], t) 
   309         Abs (_, _, _) => ([], t) 
   310       | _ => raise TERM ("dest_plain_fun", [t]))
   310       | _ => raise TERM ("dest_fun_upds", [t]))
   311   | SOME (t0, (t1, t2)) => apfst (cons (t1, t2)) (dest_plain_fun t0)
   311   | SOME (t0, (t1, t2)) => apfst (cons (t1, t2)) (dest_fun_upds t0)
   312 
   312 
   313 fun make_plain_fun T1 T2 (tps, t) = fold_rev (mk_fun_upd T1 T2) tps t
   313 fun make_fun_upds T1 T2 (tps, t) = fold_rev (mk_fun_upd T1 T2) tps t
   314 
   314 
   315 fun make_set T1 [] = Const (@{const_abbrev Set.empty}, T1 --> @{typ bool})
   315 fun make_set T1 [] = Const (@{const_abbrev Set.empty}, T1 --> @{typ bool})
   316   | make_set T1 ((_, @{const False}) :: tps) = make_set T1 tps
   316   | make_set T1 ((_, @{const False}) :: tps) = make_set T1 tps
   317   | make_set T1 ((t1, @{const True}) :: tps) =
   317   | make_set T1 ((t1, @{const True}) :: tps) =
   318     Const (@{const_name insert}, T1 --> (T1 --> @{typ bool}) --> T1 --> @{typ bool})
   318     Const (@{const_name insert}, T1 --> (T1 --> @{typ bool}) --> T1 --> @{typ bool})
   342     fun process_args t = case strip_comb t of
   342     fun process_args t = case strip_comb t of
   343       (c as Const (_, _), ts) => list_comb (c, map post_process_term ts) 
   343       (c as Const (_, _), ts) => list_comb (c, map post_process_term ts) 
   344   in
   344   in
   345     case fastype_of t of
   345     case fastype_of t of
   346       Type (@{type_name fun}, [T1, T2]) =>
   346       Type (@{type_name fun}, [T1, T2]) =>
   347         (case try dest_plain_fun t of
   347         (case try dest_fun_upds t of
   348           SOME (tps, t) =>
   348           SOME (tps, t) =>
   349             (map (pairself post_process_term) tps, map_Abs post_process_term t)
   349             (map (pairself post_process_term) tps, map_Abs post_process_term t)
   350             |> (case T2 of
   350             |> (case T2 of
   351               @{typ bool} => 
   351               @{typ bool} => 
   352                 (case t of
   352                 (case t of
   353                    Abs(_, _, @{const True}) => fst #> rev #> make_set T1
   353                    Abs(_, _, @{const True}) => fst #> rev #> make_set T1
   354                  | Abs(_, _, @{const False}) => fst #> rev #> make_coset T1
   354                  | Abs(_, _, @{const False}) => fst #> rev #> make_coset T1
       
   355                  | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> rev #> make_set T1
   355                  | _ => raise TERM ("post_process_term", [t]))
   356                  | _ => raise TERM ("post_process_term", [t]))
   356             | Type (@{type_name option}, _) =>
   357             | Type (@{type_name option}, _) =>
   357                 (case t of
   358                 (case t of
   358                   Abs(_, _, Const(@{const_name None}, _)) => fst #> (make_map T1 T2)
   359                   Abs(_, _, Const(@{const_name None}, _)) => fst #> make_map T1 T2
   359                 | _ => make_plain_fun T1 T2) 
   360                 | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> make_map T1 T2
   360             | _ => make_plain_fun T1 T2)
   361                 | _ => make_fun_upds T1 T2) 
       
   362             | _ => make_fun_upds T1 T2)
   361         | NONE => raise TERM ("post_process_term", [t]))
   363         | NONE => raise TERM ("post_process_term", [t]))
   362     | _ => process_args t
   364     | _ => process_args t
   363   end
   365   end
   364 
   366 
   365 (** generator compiliation **)
   367 (** generator compiliation **)