src/HOL/ex/Quickcheck.thy
changeset 26589 43cb72871897
parent 26325 6ecae5c8175b
child 26829 229e8078b1e0
equal deleted inserted replaced
26588:d83271bfaba5 26589:43cb72871897
    40   fun mk_collapse thy ty = Sign.mk_const thy
    40   fun mk_collapse thy ty = Sign.mk_const thy
    41     (@{const_name collapse}, [@{typ seed}, ty]);
    41     (@{const_name collapse}, [@{typ seed}, ty]);
    42   fun term_ty ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"});
    42   fun term_ty ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"});
    43   fun mk_split thy ty ty' = Sign.mk_const thy
    43   fun mk_split thy ty ty' = Sign.mk_const thy
    44     (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, StateMonad.liftT (term_ty ty') @{typ seed}]);
    44     (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, StateMonad.liftT (term_ty ty') @{typ seed}]);
    45   fun mk_mbind_split thy ty ty' t t' =
    45   fun mk_scomp_split thy ty ty' t t' =
    46     StateMonad.mbind (term_ty ty) (term_ty ty') @{typ seed} t
    46     StateMonad.scomp (term_ty ty) (term_ty ty') @{typ seed} t
    47       (mk_split thy ty ty' $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')))
    47       (mk_split thy ty ty' $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')))
    48   fun mk_cons thy this_ty (c, args) =
    48   fun mk_cons thy this_ty (c, args) =
    49     let
    49     let
    50       val tys = map (fst o fst) args;
    50       val tys = map (fst o fst) args;
    51       val c_ty = tys ---> this_ty;
    51       val c_ty = tys ---> this_ty;
    57         (list_comb (c, map (fn k => Bound (k + 1)) t_indices))
    57         (list_comb (c, map (fn k => Bound (k + 1)) t_indices))
    58         |> map_aterms (fn t as Bound _ => t $ @{term "()"} | t => t));
    58         |> map_aterms (fn t as Bound _ => t $ @{term "()"} | t => t));
    59       val return = StateMonad.return (term_ty this_ty) @{typ seed}
    59       val return = StateMonad.return (term_ty this_ty) @{typ seed}
    60         (HOLogic.mk_prod (c_t, t_t));
    60         (HOLogic.mk_prod (c_t, t_t));
    61       val t = fold_rev (fn ((ty, _), random) =>
    61       val t = fold_rev (fn ((ty, _), random) =>
    62         mk_mbind_split thy ty this_ty random)
    62         mk_scomp_split thy ty this_ty random)
    63           args return;
    63           args return;
    64       val is_rec = exists (snd o fst) args;
    64       val is_rec = exists (snd o fst) args;
    65     in (is_rec, StateMonad.run (term_ty this_ty) @{typ seed} t) end;
    65     in (is_rec, StateMonad.run (term_ty this_ty) @{typ seed} t) end;
    66   fun mk_conss thy ty [] = NONE
    66   fun mk_conss thy ty [] = NONE
    67     | mk_conss thy ty [(_, t)] = SOME t
    67     | mk_conss thy ty [(_, t)] = SOME t
   266       $ result $ @{term "None \<Colon> term list option"} $ (@{term "Some \<Colon> term list \<Rightarrow> term list option "} $ terms);
   266       $ result $ @{term "None \<Colon> term list option"} $ (@{term "Some \<Colon> term list \<Rightarrow> term list option "} $ terms);
   267     val return = @{term "Pair \<Colon> term list option \<Rightarrow> seed \<Rightarrow> term list option \<times> seed"};
   267     val return = @{term "Pair \<Colon> term list option \<Rightarrow> seed \<Rightarrow> term list option \<times> seed"};
   268     fun mk_termtyp ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"});
   268     fun mk_termtyp ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"});
   269     fun mk_split ty = Sign.mk_const thy
   269     fun mk_split ty = Sign.mk_const thy
   270       (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, StateMonad.liftT @{typ "term list option"} @{typ seed}]);
   270       (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, StateMonad.liftT @{typ "term list option"} @{typ seed}]);
   271     fun mk_mbind_split ty t t' =
   271     fun mk_scomp_split ty t t' =
   272       StateMonad.mbind (mk_termtyp ty) @{typ "term list option"} @{typ seed} t (*FIXME*)
   272       StateMonad.scomp (mk_termtyp ty) @{typ "term list option"} @{typ seed} t (*FIXME*)
   273         (mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')));
   273         (mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')));
   274     fun mk_bindclause (_, _, i, ty) = mk_mbind_split ty
   274     fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty
   275       (Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i)
   275       (Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i)
   276     val t = fold_rev mk_bindclause bounds (return $ check);
   276     val t = fold_rev mk_bindclause bounds (return $ check);
   277   in Abs ("n", @{typ index}, t) end;
   277   in Abs ("n", @{typ index}, t) end;
   278 
   278 
   279 fun compile_generator_expr thy prop tys =
   279 fun compile_generator_expr thy prop tys =